map — Mathlib

English

A function preserving bottom and infimum that maps disjoint elements to disjoint images preserves disjointness.

Русский

Функция, сохраняющая нижний элемент и Inf, сохраняет несоприкосновение элементов.

LaTeX

$$$[OrderBot\;\alpha] [OrderBot\;\beta] [BotHomClass F \alpha \beta] [InfHomClass F \alpha \beta] \{a,b: \alpha\} \; (f:\,F)\; \; h: Disjoint(a,b) \Rightarrow Disjoint(f(a),f(b))$$$

Lean4

theorem map [OrderBot α] [OrderBot β] [BotHomClass F α β] [InfHomClass F α β] {a b : α} (f : F) (h : Disjoint a b) :
    Disjoint (f a) (f b) := by rw [disjoint_iff, ← map_inf, h.eq_bot, map_bot]

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