Mathlib Map

Theorems · Theorem · order theory

WithTop.sSup_eq

∀ {α : Type u_1} [inst : LE α] [inst_1 : SupSet α] {s : Set (WithTop α)},
  ⊤ ∉ s → BddAbove (WithTop.some ⁻¹' s) → sSup s = ↑(sSup (WithTop.some ⁻¹' s))
Defined in
Mathlib.Order.ConditionallyCompleteLattice.Basic
Cited by
1 results in Mathlib
Foundations
Depth 13 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
LESupSet
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

WithTop.sSup_empty · cited by 0WithTop.sSup_emptySet · cited by 53352SetTop.top · cited by 9680Top.topSet.preimage · cited by 4946Set.preimageWithTop · cited by 3754WithTopWithTop.some · cited by 1128WithTop.someSupSet.sSup · cited by 954SupSet.sSupBddAbove · cited by 620BddAboveSupSet · cited by 154SupSetWithTop.sSup_eqCITED BYCITES

Cites8

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
  • Top.topstatement and proof · cited by 9,680
  • Set.preimagestatement and proof · cited by 4,946
  • WithTopstatement and proof · cited by 3,754
  • WithTop.somestatement and proof · cited by 1,128
  • SupSet.sSupstatement · cited by 954
  • BddAbovestatement and proof · cited by 620
  • SupSetstatement and proof · cited by 154

Cited by1

Results whose statement or proof uses this declaration.