Theorems · Theorem
Equiv.forall_congr_left
∀ {α : Sort u} {β : Sort v} {p : α → Prop} (e : α ≃ β), (∀ (a : α), p a) ↔ ∀ (b : β), p (e.symm b)- Defined in
- Mathlib.Logic.Equiv.Defs
- Cited by
- 41 results in Mathlib
- Foundations
- Depth 16 from the axioms · uses Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Equivstatement and proof · cited by 8,337
- Equiv.symmstatement and proof · cited by 3,681
- Equiv.forall_congr_rightproof · cited by 28
Cited by41
Results whose statement or proof uses this declaration.
- Equiv.forall_congrproof · cited by 22
- Equiv.forall_congr'proof · cited by 5
- Ring.krullDimLE_zero_iffproof · cited by 5
- CategoryTheory.Presieve.isSheafFor_iff_bijective_shrinkFunctor_ι_compproof · cited by 4
- Ideal.height_le_iffproof · cited by 3
- Ring.krullDimLE_one_iff_of_isPrime_botproof · cited by 3
- CategoryTheory.Presieve.isSheafFor_iff_yonedaSheafConditionproof · cited by 3
- ZSpan.fundamentalDomain_reindexproof · cited by 2
- AlgebraicGeometry.sourceAffineLocally_morphismRestrictproof · cited by 2
- FirstOrder.realize_genericPolyMapSurjOnOfInjOnproof · cited by 2
- CategoryTheory.Presieve.isSheafFor_singletonproof · cited by 2
- NumberField.Units.finrank_mul_regOfFamily_eq_detproof · cited by 2