English
Infimum structure on WithTop α is defined by taking a top element when S is empty or not bounded below, otherwise it is the embedding of the Infimum in α of the preimage of S.
Русский
Структура infimum на WithTop α определяется как ⊤ в случае пустого множества или если множество не ограничено снизу; иначе это вложение инфимума из α для предобраза S.
LaTeX
$$$$ \text{InfSet}_{WithTop \ α} (S) = \begin{cases} \top, & S \subseteq \{\top\} \ \lor\ \neg \mathrm{BddBelow}(S) \\ \uparrow \operatorname{sInf}\left( \{a \in \alpha \mid \uparrow a \in S\} \right), & \text{иначе} \end{cases} $$$$
Lean4
noncomputable instance instInfSet [InfSet α] : InfSet (WithTop α) :=
⟨fun S => if S ⊆ {⊤} ∨ ¬BddBelow S then ⊤ else ↑(sInf ((fun (a : α) ↦ ↑a) ⁻¹' S : Set α))⟩
