iciSupHom — Mathlib

English

Principal upper sets (Ici) form a SupHom from α to the lattice of upper sets: Ici: α → UpperSet α preserves suprema.

Русский

Принципиальные верхние множества (Ici) образуют SupHom от α к частично упорядоченному множеству верхних множеств: Ici сохраняет супремумы.

LaTeX

$$$ \text{Ici} : \alpha \to \text{SupHom}(\alpha, \text{UpperSet}(\alpha)) $$$

Lean4

/-- `UpperSet.Ici` as a `SupHom`. -/
def iciSupHom : SupHom α (UpperSet α) :=
  ⟨Ici, Ici_sup⟩

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