Mathlib Map

Theorems · Theorem · order theory

Set.Icc_subset_Iic_self

∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Icc a b ⊆ Set.Iic b
Defined in
Mathlib.Order.Interval.Set.Basic
Cited by
10 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.

IsLowerSet.ordConnected · cited by 5IsLowerSet.ordConnectedeVariationOn.sum_le_of_monotoneOn_Iic · cited by 5eVariationOn.sum_le_of_mo…Iio_mem_nhdsSet_Icc · cited by 4Iio_mem_nhdsSet_IccMeasureTheory.integral_Iic_of_hasDerivAt_of_tendsto · cited by 3MeasureTheory.integral_Ii…MeasureTheory.integrableOn_Iic_iff_integrableAtFilter_atBot · cited by 3MeasureTheory.integrableO…WithTop.image_coe_Icc · cited by 3WithTop.image_coe_IcceVariationOn.Icc_add_Icc · cited by 2eVariationOn.Icc_add_IccFinset.Icc_subset_Iic_self · cited by 1Finset.Icc_subset_Iic_selfSet.bounded_le_Icc · cited by 0Set.bounded_le_IccSet.bounded_lt_Icc · cited by 0Set.bounded_lt_IccSet · cited by 53352SetPreorder · cited by 7952PreorderSet.Icc · cited by 1702Set.IccSet.Iic · cited by 1111Set.IicSet.Icc_subset_Iic_selfCITED BYCITES

Cites4

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

Cited by10

Results whose statement or proof uses this declaration.