Theorems · Theorem · order theory

csSup_Ioc

∀ {α : Type u_1} [inst : ConditionallyCompletePartialOrderSup α] {a b : α}, a < b → sSup (Set.Ioc a b) = b

Defined in: Mathlib.Order.ConditionallyCompletePartialOrder.Basic
Cited by: 0 results in Mathlib
Foundations: Depth 14 from the axioms · uses propext, Quot.sound
Assumes: ConditionallyCompletePartialOrderSup

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites5

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

Set.Iocstatement · cited by 971
SupSet.sSupstatement · cited by 954
ConditionallyCompletePartialOrderSupstatement and proof · cited by 52
IsGreatest.csSup_eqproof · cited by 9
isGreatest_Iocproof · cited by 2

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.