codisjoint_iff — Mathlib

English

In a product with top, Codisjoint(x,y) holds iff both coordinates are codisjoint.

Русский

В произведении с верхом Codisjoint(x,y) эквивалентно кодисjoint(x1,y1) и Codisjoint(x2,y2).

LaTeX

$$$$ \text{Codisjoint}((a,b),(a',b')) \Leftrightarrow \text{Codisjoint}(a,a') \land \text{Codisjoint}(b,b'). $$$$

Lean4

protected theorem codisjoint_iff [OrderTop α] [OrderTop β] {x y : α × β} :
    Codisjoint x y ↔ Codisjoint x.1 y.1 ∧ Codisjoint x.2 y.2 :=
  @Prod.disjoint_iff αᵒᵈ βᵒᵈ _ _ _ _ _ _

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