Mathlib Map

Theorems · Theorem · order theory

Set.sInter_range

∀ {β : Type u_2} {ι : Sort u_5} (f : ι → Set β), ⋂₀ Set.range f = ⋂ x, f x
Defined in
Mathlib.Data.Set.Lattice
Cited by
16 results in Mathlib
Foundations
Depth 6 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

IsGδ.iInter_of_isOpen · cited by 5IsGδ.iInter_of_isOpenconvex_iInter · cited by 3convex_iIntercountable_iInter_mem · cited by 3countable_iInter_meminterior_iInter_of_finite · cited by 2interior_iInter_of_finiteFilter.cardinal_iInter_mem · cited by 2Filter.cardinal_iInter_memAbsConvex.iInter · cited by 1AbsConvex.iInterstarConvex_iInter · cited by 1starConvex_iInterFilter.iInter_mem' · cited by 1Filter.iInter_mem'IsClub.iInter · cited by 1IsClub.iInterIsClub.iInter_of_cof_le_one · cited by 1IsClub.iInter_of_cof_le_o…DirSupClosed.iInter · cited by 0DirSupClosed.iInterDirSupClosedOn.iInter · cited by 0DirSupClosedOn.iInterIsSemilinearSet.iInter · cited by 0IsSemilinearSet.iInterbaire_of_finite · cited by 0baire_of_finiteIsClub.iInter_of_countable · cited by 0IsClub.iInter_of_countableSet · cited by 53352SetSet.range · cited by 4705Set.rangeSet.iInter · cited by 1084Set.iInterSet.sInter · cited by 225Set.sInterSet.sInter_rangeCITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by16

Results whose statement or proof uses this declaration.