Theorems · Definition · order theory

subsetSupSet

{α : Type u_2} → (s : Set α) → [Preorder α] → [SupSet α] → [Inhabited ↑s] → SupSet ↑s

SupSet structure on a nonempty subset s of a preorder with SupSet. This definition is non-canonical (it uses default s); it should be used only as here, as an auxiliary instance in the construction of the ConditionallyCompleteLinearOrder structure.

Defined in

Mathlib.Order.CompleteLatticeIntervals

Cited by

4 results in Mathlib

Foundations

Depth 12 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PreorderSupSetInhabited