semiconjBy_iff — Mathlib

English

A pi-valued triple x,y,z is semiconjugate precisely when each coordinate is semiconjugate: SemiconjBy x y z if and only if ∀ i, SemiconjBy (x i) (y i) (z i).

Русский

Тройка значений x,y,z в пи-объектах является полусопряжённой тогда и только тогда, когда каждая координата удовлетворяет той же условию: SemiconjBy x y z ⇔ ∀ i, SemiconjBy (x i) (y i) (z i).

LaTeX

$$$\mathrm{SemiconjBy}(x,y,z) \iff \forall i, \mathrm{SemiconjBy}(x_i, y_i, z_i)$$$

Lean4

@[to_additive]
theorem semiconjBy_iff {x y z : ∀ i, f i} : SemiconjBy x y z ↔ ∀ i, SemiconjBy (x i) (y i) (z i) :=
  funext_iff

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