Theorems · Theorem · order theory

Set.uIoo_of_ge

∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, b ≤ a → Set.uIoo a b = Set.Ioo b a

Defined in: Mathlib.Order.Interval.Set.UnorderedInterval
Cited by: 3 results in Mathlib
Foundations: Depth 19 from the axioms · uses propext
Assumes: LinearOrder

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
LinearOrderstatement and proof · cited by 8,572
Set.Ioostatement and proof · cited by 1,214
sup_eq_leftproof · cited by 71
Set.uIoostatement · cited by 68
inf_eq_rightproof · cited by 64

Cited by3

Results whose statement or proof uses this declaration.

Set.uIoo_of_gtproof · cited by 2
Set.uIoo_eq_unionproof · cited by 0
intervalIntegral.integral_deriv_eq_sub_uIooproof · cited by 0