isCompl_iff — Mathlib

English

An element of a product is a complement iff its coordinates are complements.

Русский

Элемент произведения является комплементом тогда и только тогда, когда его координаты являются комплементами.

LaTeX

$$$$ IsCompl((a,b),(c,d)) \iff IsCompl(a,c) \land IsCompl(b,d). $$$$

Lean4

protected theorem isCompl_iff [BoundedOrder α] [BoundedOrder β] {x y : α × β} :
    IsCompl x y ↔ IsCompl x.1 y.1 ∧ IsCompl x.2 y.2 := by
  simp_rw [isCompl_iff, Prod.disjoint_iff, Prod.codisjoint_iff, and_and_and_comm]

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