disjoint_map_orderIso_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem disjoint_map_orderIso_iff [SemilatticeInf α] [OrderBot α] [SemilatticeInf β] [OrderBot β] {a b : α}
    (f : α ≃o β) : Disjoint (f a) (f b) ↔ Disjoint 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⟩

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