English
For an inhabited set s, the supremum in the induced substructure on s is given by a conditional rule: if t is nonempty, bounded above, and the supremum of the image lies in s, then the supremum is that image’s supremum; otherwise it is the default element.
Русский
Для непустого множества s верхняя граница в индуцированной подпредельной структуре задаётся по правилу: если t непусто, ограничено сверху и sSup, полученное на образе t, лежит в s, то взятое значение является сSup; иначе возвращается дефолт.
LaTeX
$$$$ \operatorname{sSup}_{s}(t) = \begin{cases} \langle \operatorname{sSup}((\uparrow)''t), \text{proof} \rangle, & t\neq\emptyset \land \operatorname{BddAbove}(t) \land \operatorname{sSup}((\uparrow)''t) \in s \\ \text{default}, & \text{otherwise} \end{cases} $$$$
Lean4
@[simp]
theorem subset_sSup_def [Inhabited s] :
@sSup s _ = fun t =>
if ht : t.Nonempty ∧ BddAbove t ∧ sSup ((↑) '' t : Set α) ∈ s then ⟨sSup ((↑) '' t : Set α), ht.2.2⟩
else default :=
rfl
