Mathlib Map

Theorems · Theorem · order theory

Set.subset_iInter

∀ {β : Type u_2} {ι : Sort u_5} {t : Set β} {s : ι → Set β}, (∀ (i : ι), t ⊆ s i) → t ⊆ ⋂ i, s i
Defined in
Mathlib.Data.Set.Lattice
Cited by
17 results in Mathlib
Foundations
Depth 60 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Set.subset_iInter₂ · cited by 9Set.subset_iInter₂MeasureTheory.OuterMeasure.exists_measurable_superset_eq_trim · cited by 4OuterMeasure.exists_measu…MeasureTheory.OuterMeasure.exists_measurable_superset_forall_eq_trim · cited by 3OuterMeasure.exists_measu…AlgebraicGeometry.Scheme.IdealSheafData.zeroLocus_inter_subset_supportSet · cited by 2IdealSheafData.zeroLocus_…interior_iInter · cited by 2interior_iInterMeasureTheory.hahn_decomposition · cited by 2MeasureTheory.hahn_decomp…Perfect.subset_perfectKernel · cited by 1Perfect.subset_perfectKer…CantorBendixson.perfectKernel_eq_iteratedDerivedSet_of_mem_fixedPoints · cited by 1CantorBendixson.perfectKe…MeasureTheory.Measure.measure_toMeasurable_inter_of_sum · cited by 1Measure.measure_toMeasura…connectedComponent_subset_iInter_isClopen · cited by 1connectedComponent_subset…interior_iInter_subset · cited by 1interior_iInter_subsetSet.iInter_mono' · cited by 1Set.iInter_mono'Matroid.IsFlat.iInter · cited by 1IsFlat.iInterMeasureTheory.MeasurablySeparable.iUnion · cited by 1MeasurablySeparable.iUnionSet.iInter_subset_iInter₂ · cited by 1Set.iInter_subset_iInter₂Set · cited by 53352SetSet.iInter · cited by 1084Set.iInterle_iInf · cited by 102le_iInfSet.subset_iInterCITED BYCITES

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
  • le_iInfproof · cited by 102

Cited by17

Results whose statement or proof uses this declaration.