Mathlib Map

Theorems · Theorem · order theory

Set.Ioi_inter_Iic

∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ioi a ∩ Set.Iic b = Set.Ioc a b
Defined in
Mathlib.Order.Interval.Set.Basic
Cited by
13 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_Ioc · cited by 10interior_Iocconvex_Ioc · cited by 8convex_IocOrder.Icc_succ_left_of_not_isMax · cited by 2Order.Icc_succ_left_of_no…Set.Ioi_sdiff_Ioi · cited by 2Set.Ioi_sdiff_IoiSet.image_subtype_val_Ioi_Iic · cited by 1Set.image_subtype_val_Ioi…nhdsLE_eq_iInf_principal · cited by 1nhdsLE_eq_iInf_principalOrder.Ioo_succ_right_of_not_isMax · cited by 1Order.Ioo_succ_right_of_n…Set.Ioc_add_bij · cited by 1Set.Ioc_add_bijOrder.Ioc_pred_left_eq_insert_of_not_isMin · cited by 1Order.Ioc_pred_left_eq_in…Set.pi_univ_Ioc_update_left · cited by 1Set.pi_univ_Ioc_update_le…Set.pi_univ_Ioc_update_right · cited by 1Set.pi_univ_Ioc_update_ri…Set.Ioc_inter_Iic · cited by 0Set.Ioc_inter_IicEReal.preimage_coe_Ioc_bot · cited by 0EReal.preimage_coe_Ioc_botSet · cited by 53352SetPreorder · cited by 7952PreorderSet.Ioi · cited by 1463Set.IoiSet.Iic · cited by 1111Set.IicSet.Ioc · cited by 971Set.IocSet.Ioi_inter_IicCITED 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.Iicstatement · cited by 1,111
  • Set.Iocstatement · cited by 971

Cited by13

Results whose statement or proof uses this declaration.