Mathlib Map

Theorems · Theorem · order theory

Set.Ioi_inter_Iio

∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ioi a ∩ Set.Iio b = Set.Ioo a b
Defined in
Mathlib.Order.Interval.Set.Basic
Cited by
16 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.

interior_Icc · cited by 37interior_IccIoo_mem_nhdsGT · cited by 20Ioo_mem_nhdsGTinterior_Ico · cited by 12interior_Icointerior_Ioc · cited by 10interior_IocSet.image_subtype_val_Ioi_Iio · cited by 3Set.image_subtype_val_Ioi…Order.Ico_succ_left_of_not_isMax · cited by 2Order.Ico_succ_left_of_no…WithTop.image_coe_Ioi · cited by 2WithTop.image_coe_Ioiconvex_Ioo · cited by 2convex_IooFin.image_val_Ioi · cited by 2Fin.image_val_IoiOrder.Ioo_succ_right_of_not_isMax · cited by 1Order.Ioo_succ_right_of_n…Set.Ioo_add_bij · cited by 1Set.Ioo_add_bijSet.Ioi_sdiff_Ici · cited by 1Set.Ioi_sdiff_IciOrder.Ioo_pred_left_eq_insert_of_not_isMin · cited by 1Order.Ioo_pred_left_eq_in…EReal.preimage_coe_Ioo_bot · cited by 0EReal.preimage_coe_Ioo_botEReal.preimage_coe_Ioo_bot_top · cited by 0EReal.preimage_coe_Ioo_bo…Set · cited by 53352SetPreorder · cited by 7952PreorderSet.Ioi · cited by 1463Set.IoiSet.Ioo · cited by 1214Set.IooSet.Iio · cited by 1166Set.IioSet.Ioi_inter_IioCITED 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 · cited by 1,463
  • Set.Ioostatement · cited by 1,214
  • Set.Iiostatement · cited by 1,166

Cited by16

Results whose statement or proof uses this declaration.