Mathlib Map

Theorems · Theorem · order theory

Set.left_mem_Icc

∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ∈ Set.Icc a b ↔ a ≤ b
Defined in
Mathlib.Order.Interval.Set.Basic
Cited by
67 results in Mathlib
Foundations
Depth 7 from the axioms · uses propext
Assumes
Preorder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Set.nonempty_Icc · cited by 21Set.nonempty_IccReal.arcsin_of_le_neg_one · cited by 7Real.arcsin_of_le_neg_oneSet.projIcc_of_le_left · cited by 5Set.projIcc_of_le_leftintermediate_value_Icc · cited by 4intermediate_value_IccSet.IccExtend_of_le_left · cited by 4Set.IccExtend_of_le_leftisLeast_Icc · cited by 4isLeast_IccSet.Ioc_union_left · cited by 3Set.Ioc_union_leftMonotoneOn.mapsTo_Icc · cited by 3MonotoneOn.mapsTo_Iccintermediate_value_Icc' · cited by 3intermediate_value_Icc'PhragmenLindelof.horizontal_strip · cited by 3PhragmenLindelof.horizont…hasSum_zeta_nat · cited by 3hasSum_zeta_natAntitoneOn.mapsTo_Icc · cited by 3AntitoneOn.mapsTo_IccSet.compl_ordConnectedSection_ordSeparatingSet_mem_nhdsGE · cited by 2Set.compl_ordConnectedSec…StrictAntiOn.mapsTo_Ico · cited by 2StrictAntiOn.mapsTo_IcoStrictAntiOn.mapsTo_Ioc · cited by 2StrictAntiOn.mapsTo_IocSet · cited by 53352SetPreorder · cited by 7952PreorderSet.Icc · cited by 1702Set.IccSet.left_mem_IccCITED BYCITES

Cites3

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
  • Set.Iccstatement · cited by 1,702

Cited by69

Results whose statement or proof uses this declaration.