English
For inhabited s, the infimum in the induced substructure on s is given by a conditional rule mirroring sSup_def with sInf and BddBelow.
Русский
Для непустого s инфimum в индуцированной подпредельной структуре задаётся по аналогии с определением sSup_def, используя sInf и BddBelow.
LaTeX
$$$$ \operatorname{sInf}_{s}(t) = \begin{cases} \langle \operatorname{sInf}((\uparrow)''t), \text{proof} \rangle, & t\neq\emptyset \land \operatorname{BddBelow}(t) \land \operatorname{sInf}((\uparrow)''t) \in s \\ \text{default}, & \text{otherwise} \end{cases} $$$$
Lean4
@[simp]
theorem subset_sInf_def [Inhabited s] :
@sInf s _ = fun t =>
if ht : t.Nonempty ∧ BddBelow t ∧ sInf ((↑) '' t : Set α) ∈ s then ⟨sInf ((↑) '' t : Set α), ht.2.2⟩
else default :=
rfl
