Mathlib Map

Theorems · Theorem · order theory

Set.Iio_subset_Iic_self

∀ {α : Type u_1} [inst : Preorder α] {a : α}, Set.Iio a ⊆ Set.Iic a
Defined in
Mathlib.Order.Interval.Set.Basic
Cited by
21 results in Mathlib
Foundations
Depth 6 from the axioms · uses no axioms
Assumes
Preorder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Iic_mem_nhds · cited by 6Iic_mem_nhdsnhds_bot_basis_Iic · cited by 4nhds_bot_basis_IicContinuousWithinAt.leftLim_eq · cited by 4ContinuousWithinAt.leftLi…Iic_mem_nhdsSet_Icc · cited by 3Iic_mem_nhdsSet_IccmapClusterPt_leftLim · cited by 3mapClusterPt_leftLimENNReal.iUnion_Iic_coe_nat · cited by 3ENNReal.iUnion_Iic_coe_natFilter.atBot_basis_Iio · cited by 3Filter.atBot_basis_IioIic_mem_nhdsSet_Ico · cited by 2Iic_mem_nhdsSet_IcoSet.mem_Iic_of_Iio · cited by 2Set.mem_Iic_of_IiohasBasis_nhdsSet_Iic_Iic · cited by 2hasBasis_nhdsSet_Iic_IicisCofinal_iff_iUnion_Iio_eq_univ · cited by 1isCofinal_iff_iUnion_Iio_…iUnion_Iic_of_not_bddAbove_range · cited by 1iUnion_Iic_of_not_bddAbov…IsLowerSet.Iio_subset · cited by 1IsLowerSet.Iio_subsetSet.Iio_subset_Iic · cited by 1Set.Iio_subset_IicFinset.Iio_subset_Iic_self · cited by 1Finset.Iio_subset_Iic_selfSet · cited by 53352SetPreorder · cited by 7952Preorderle_of_lt · cited by 1175le_of_ltSet.Iio · cited by 1166Set.IioSet.Iic · cited by 1111Set.IicSet.Iio_subset_Iic_selfCITED BYCITES

Cites5

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

  • Setstatement · cited by 53,352
  • Preorderstatement and proof · cited by 7,952
  • le_of_ltproof · cited by 1,175
  • Set.Iiostatement and proof · cited by 1,166
  • Set.Iicstatement · cited by 1,111

Cited by21

Results whose statement or proof uses this declaration.