map_orderIso — Mathlib

English

If a and b are codisjoint in α, then f(a) and f(b) are codisjoint in β under a order-embedding f.

Русский

Если a и b кодиссоразделены в α, то f(a) и f(b) кодиссоразделены в β под вложением порядка f.

LaTeX

$$$ a \vee b = \top \quad\Rightarrow\quad f(a) \vee f(b) = \top $$$

Lean4

/-- Note that this goal could also be stated `(Codisjoint on f) a b` -/
theorem map_orderIso [SemilatticeSup α] [OrderTop α] [SemilatticeSup β] [OrderTop β] {a b : α} (f : α ≃o β)
    (ha : Codisjoint a b) : Codisjoint (f a) (f b) :=
  by
  rw [codisjoint_iff_le_sup, ← f.map_sup, ← f.map_top]
  exact f.monotone ha.top_le

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