iicsInfHom — Mathlib

English

The Iic construction provides an sInfHom from α to LowerSet α, sending s to Iic s and preserving infima via image().

Русский

Конструкция Iic образует sInfHom от α к LowerSet α, отображая s в Iic s и сохраняет infima через отображение.

LaTeX

$$$ \mathrm{iicsInfHom} : \alpha \to \mathrm{sInfHom}(\alpha, \mathrm{LowerSet}(\alpha)) $$$

Lean4

/-- `LowerSet.Iic` as an `sInfHom`. -/
def iicsInfHom : sInfHom α (LowerSet α) :=
  ⟨Iic, fun s => (Iic_sInf s).trans sInf_image.symm⟩

Похожие утверждения