Theorems · Theorem
Equiv.forall_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
- 22 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.forall_congr_leftproof · cited by 41
Cited by22
Results whose statement or proof uses this declaration.
- PowerSeries.WithPiTopology.tendsto_iff_coeff_tendstoproof · cited by 5
- ContinuousLinearMapWOT.tendsto_iff_forall_inner_apply_tendstoproof · cited by 3
- AddEquiv.isWeaklyRegular_congrproof · cited by 3
- AddSubgroup.index_eq_two_iff'proof · cited by 2
- isIrreducible_iff_sUnion_isClosedproof · cited by 2
- RelIso.wellQuasiOrdered_iffproof · cited by 2
- Equiv.forall₂_congrproof · cited by 2
- Equiv.existsUnique_congr_rightproof · cited by 1
- AddSubgroup.index_dvd_two_iff'proof · cited by 1
- AddAction.isBlock_topproof · cited by 1
- Subgroup.map_equiv_normalizer_eqproof · cited by 1
- map_equiv_traceDualproof · cited by 1