Mathlib Map

Theorems · Theorem · order theory

subset_sSup_of_within

∀ {α : Type u_2} (s : Set α) [inst : Preorder α] [inst_1 : SupSet α] [inst_2 : Inhabited ↑s] {t : Set ↑s},
  t.Nonempty → BddAbove t → sSup (Subtype.val '' t) ∈ s → sSup (Subtype.val '' t) = ↑(sSup t)
Defined in
Mathlib.Order.CompleteLatticeIntervals
Cited by
1 results in Mathlib
Foundations
Depth 13 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
PreorderSupSetInhabited
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

NNReal.coe_sSup · cited by 5NNReal.coe_sSupSet · cited by 53352SetPreorder · cited by 7952PreorderSet.Elem · cited by 7166Set.ElemSet.image · cited by 5609Set.imageSet.Nonempty · cited by 2627Set.NonemptySupSet.sSup · cited by 954SupSet.sSupBddAbove · cited by 620BddAboveSupSet · cited by 154SupSetsubsetSupSet · cited by 4subsetSupSetsubset_sSup_of_withinCITED BYCITES

Cites9

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
  • Preorderstatement and proof · cited by 7,952
  • Set.Elemstatement and proof · cited by 7,166
  • Set.imagestatement and proof · cited by 5,609
  • Set.Nonemptystatement and proof · cited by 2,627
  • SupSet.sSupstatement and proof · cited by 954
  • BddAbovestatement and proof · cited by 620
  • SupSetstatement and proof · cited by 154
  • subsetSupSetstatement · cited by 4

Cited by1

Results whose statement or proof uses this declaration.