map — Mathlib

English

A map preserving top and sup sends codisjoint elements to codisjoint images.

Русский

Функция, сохраняющая верхние пределы и сумы, сохраняет кодиспособность разности.

LaTeX

$$$[OrderTop\;\alpha] [OrderTop\;\beta] [TopHomClass F \alpha \beta] [SupHomClass F \alpha \beta] {a b : \alpha} (f : F) (h : Codisjoint a b) : Codisjoint (f a) (f b)$$$

Lean4

theorem map [OrderTop α] [OrderTop β] [TopHomClass F α β] [SupHomClass F α β] {a b : α} (f : F) (h : Codisjoint a b) :
    Codisjoint (f a) (f b) := by rw [codisjoint_iff, ← map_sup, h.eq_top, map_top]

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