map_sup — Mathlib

English

If f is monotone and for all x,y, f(x ⊔ y) = f x ⊔ f y, then f preserves suprema.

Русский

Если f монотонна и сохраняет операцию ⊔ на парах, тогда она сохраняет верхние грани.

LaTeX

$$$ [SemilatticeSup \alpha] [SemilatticeSup \beta] {f : \alpha \to \beta} (hf : Monotone f) (x y : \alpha) : f(x \lor y) = f(x) \lor f(y)$$$

Lean4

theorem map_sup [SemilatticeSup β] {f : α → β} (hf : Monotone f) (x y : α) : f (x ⊔ y) = f x ⊔ f y :=
  (IsTotal.total x y).elim (fun h : x ≤ y => by simp only [h, hf h, sup_of_le_right]) fun h => by
    simp only [h, hf h, sup_of_le_left]

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