Theorems · Theorem · order theory
Set.iInter_congr_Prop
∀ {α : Type u_1} {p q : Prop} {f₁ : p → Set α} {f₂ : q → Set α} (pq : p ↔ q),
(∀ (x : q), f₁ ⋯ = f₂ x) → Set.iInter f₁ = Set.iInter f₂- Defined in
- Mathlib.Data.Set.Lattice
- Cited by
- 170 results in Mathlib
- Foundations
- Depth 6 from the axioms, rests on 20 definitions · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Set.iInterstatement · cited by 1,084
- iInf_congr_Propproof · cited by 218
Cited by170
Results whose statement or proof uses this declaration.
- Set.iInter_iInter_eq'proof · cited by 22
- Filter.biInter_memproof · cited by 22
- Submodule.coe_iInfproof · cited by 16
- ProbabilityTheory.iIndepFun.isProbabilityMeasureproof · cited by 14
- Subfield.coe_sInfproof · cited by 5
- ProbabilityTheory.Kernel.iIndepFun_iff_measure_inter_preimage_eq_mulproof · cited by 5
- Set.Finite.interior_biInterproof · cited by 5
- LowerSet.coe_iInfproof · cited by 4
- UpperSet.coe_iSupproof · cited by 4
- ProbabilityTheory.iIndepFun.map_fun_eq_pi_mapproof · cited by 4
- Filter.HasBasis.liminf_eq_sSup_iUnion_iInterproof · cited by 4
- MeasureTheory.measurableSet_exists_tendstoproof · cited by 4