English
For InfSet α, for a nonempty, bounded-below subset s of α, the embedding of sInf s equals the Infimum of the image of s under the embedding.
Русский
Для InfSet α, если s не пусто и ограничено снизу, вложение sInf s равно инфимума образа s под вложение.
LaTeX
$$$$ \uparrow\bigl( \operatorname{sInf} s \bigr) = \operatorname{sInf}\bigl( \{ \uparrow a \mid a \in s \} \bigr). $$$$
Lean4
theorem coe_sInf' [InfSet α] {s : Set α} (hs : s.Nonempty) (h's : BddBelow s) :
↑(sInf s) = (sInf ((fun (a : α) ↦ ↑a) '' s) : WithTop α) := by
classical
obtain ⟨x, hx⟩ := hs
change _ = ite _ _ _
split_ifs with h
· rcases h with h1 | h2
· cases h1 (mem_image_of_mem _ hx)
· exact (h2 (Monotone.map_bddBelow coe_mono h's)).elim
· rw [preimage_image_eq]
exact Option.some_injective _
