toTopHomClass — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

instance (priority := 100) toTopHomClass [LE α] [LE β] [BoundedOrder α] [BoundedOrder β] [BoundedOrderHomClass F α β] :
    TopHomClass F α β :=
  { ‹BoundedOrderHomClass F α β› with }
    -- See note [lower instance priority]

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