Mathlib Map

Theorems · Theorem · order theory

Set.Iic_inter_Ioi

∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Iic a ∩ Set.Ioi b = Set.Ioc b a
Defined in
Mathlib.Order.Interval.Set.Basic
Cited by
5 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…Order.Ioc_pred_right_of_not_isMin · cited by 2Order.Ioc_pred_right_of_n…WithBot.image_coe_Iic · cited by 1WithBot.image_coe_IicSet.Iic_sdiff_Iic · cited by 1Set.Iic_sdiff_IicisLocallyClosed_Ioc · cited by 0isLocallyClosed_IocSet · cited by 53352SetPreorder · cited by 7952PreorderSet.Ioi · cited by 1463Set.IoiSet.Iic · cited by 1111Set.IicSet.Ioc · cited by 971Set.IocSet.Iic_inter_IoiCITED 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.Ioistatement and proof · cited by 1,463
  • Set.Iicstatement and proof · cited by 1,111
  • Set.Iocstatement · cited by 971

Cited by5

Results whose statement or proof uses this declaration.