map_orderIso — Mathlib

English

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

Русский

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

LaTeX

$$$ a \perp b \quad\Rightarrow\quad f(a) \perp f(b) $$$

Lean4

/-- Note that this goal could also be stated `(Disjoint on f) a b` -/
theorem map_orderIso [SemilatticeInf α] [OrderBot α] [SemilatticeInf β] [OrderBot β] {a b : α} (f : α ≃o β)
    (ha : Disjoint a b) : Disjoint (f a) (f b) :=
  by
  rw [disjoint_iff_inf_le, ← f.map_inf, ← f.map_bot]
  exact f.monotone ha.le_bot

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