Mathlib Map

Theorems · Theorem · order theory

Set.Iic_inter_Ici

∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Iic a ∩ Set.Ici b = Set.Icc b a
Defined in
Mathlib.Order.Interval.Set.Basic
Cited by
6 results in Mathlib
Foundations
Depth 11 from the axioms · uses propext, Quot.sound
Assumes
Preorder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Order.Ioc_pred_left_of_not_isMin · cited by 2Order.Ioc_pred_left_of_no…Set.Iic_disjoint_Ici · cited by 2Set.Iic_disjoint_IciOrder.Icc_pred_right_of_not_isMin · cited by 2Order.Icc_pred_right_of_n…MeasureTheory.IntegrableOn.continuousOn_Iic_primitive_Iio · cited by 1IntegrableOn.continuousOn…Set.Icc_inter_Icc_eq_singleton · cited by 0Set.Icc_inter_Icc_eq_sing…Set.Iic_sdiff_Iio · cited by 0Set.Iic_sdiff_IioSet · cited by 53352SetPreorder · cited by 7952PreorderSet.Icc · cited by 1702Set.IccSet.Iic · cited by 1111Set.IicSet.Ici · cited by 1070Set.IciSet.Iic_inter_IciCITED 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
  • Set.Iicstatement and proof · cited by 1,111
  • Set.Icistatement and proof · cited by 1,070

Cited by6

Results whose statement or proof uses this declaration.