Mathlib Map

Theorems · Theorem · order theory

Set.Ioc_subset_Icc_self

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

intervalIntegral.integral_congr · cited by 18intervalIntegral.integral…Set.uIoc_subset_uIcc · cited by 15Set.uIoc_subset_uIccIntervalIntegrable.continuousOn_mul · cited by 8IntervalIntegrable.contin…IntervalIntegrable.mul_continuousOn · cited by 7IntervalIntegrable.mul_co…IntervalIntegrable.continuousOn_smul · cited by 6IntervalIntegrable.contin…closure_Ioc · cited by 5closure_IocintervalIntegral.integral_mono_on · cited by 5intervalIntegral.integral…MonotoneOn.intervalIntegrable · cited by 4MonotoneOn.intervalIntegr…AddCircle.volume_closedBall · cited by 4AddCircle.volume_closedBa…isGLB_Ioc · cited by 3isGLB_Iocmeasure_Ioc_lt_top · cited by 3measure_Ioc_lt_topIntervalIntegrable.smul_continuousOn · cited by 3IntervalIntegrable.smul_c…Continuous.integrableOn_Ioc · cited by 3Continuous.integrableOn_I…OrderEmbedding.image_Ioc · cited by 3OrderEmbedding.image_IocintervalIntegral.integral_nonneg_of_ae_restrict · cited by 3intervalIntegral.integral…Set · cited by 53352SetPreorder · cited by 7952PreorderSet.Icc · cited by 1702Set.Iccle_of_lt · cited by 1175le_of_ltSet.Ioc · cited by 971Set.IocSet.Ioc_subset_Icc_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
  • Set.Iccstatement · cited by 1,702
  • le_of_ltproof · cited by 1,175
  • Set.Iocstatement · cited by 971

Cited by53

Results whose statement or proof uses this declaration.