codisjoint_map_orderIso_iff — Mathlib

English

Codisjointness is preserved and reflected by an order isomorphism: Codisjoint(a,b) iff Codisjoint(f(a), f(b)).

Русский

Кодиссоразделенность сохраняется и отражается через изоморфизм порядка: Codisjoint(a,b) эквив Codisjoint(f(a), f(b)).

LaTeX

$$$ Codisjoint(a,b) \iff Codisjoint(f(a), f(b)) $$$

Lean4

@[simp]
theorem codisjoint_map_orderIso_iff [SemilatticeSup α] [OrderTop α] [SemilatticeSup β] [OrderTop β] {a b : α}
    (f : α ≃o β) : Codisjoint (f a) (f b) ↔ Codisjoint a b :=
  ⟨fun h => f.symm_apply_apply a ▸ f.symm_apply_apply b ▸ h.map_orderIso f.symm, fun h => h.map_orderIso f⟩

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