Theorems · Theorem
Equiv.exists_congr
∀ {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop} (e : α ≃ β),
(∀ (a : α), p a ↔ q (e a)) → ((∃ a, p a) ↔ ∃ b, q b)- Defined in
- Mathlib.Logic.Equiv.Defs
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 17 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Equivstatement and proof · cited by 8,337
- Equiv.symmproof · cited by 3,681
- Equiv.apply_symm_applyproof · cited by 346
- Equiv.exists_congr_leftproof · cited by 33
Cited by13
Results whose statement or proof uses this declaration.
- QuadraticMap.Equivalent.sigPos_eqproof · cited by 3
- QuasispectrumRestricts.cfcproof · cited by 2
- SpectrumRestricts.cfcproof · cited by 2
- AddSubgroup.index_eq_two_iff'proof · cited by 2
- ContextFreeGrammar.produces_reverseproof · cited by 1
- Equiv.existsUnique_congr_rightproof · cited by 1
- AddSubgroup.index_dvd_two_iff'proof · cited by 1
- FirstOrder.Language.Formula.realize_iExsproof · cited by 1
- analyticOrderAt_negproof · cited by 1
- ConcaveOn.continuousOn_tfaeproof · cited by 0
- ContextFreeGrammar.produces_reverse_commproof · cited by 0
- Subgroup.index_dvd_two_iff'proof · cited by 0