isCoprime_tfae — Mathlib

English

IsCoprime I J, Codisjoint I J, I+J=1, ∃ i∈I ∃ j∈J i+j=1, I ⊔ J = ⊤ are all equivalent (a standard TFAE).

Русский

Утверждения IsCoprime I J, Codisjoint I J, I+J=1, ∃ i∈I ∃ j∈J i+j=1 и I ⊔ J = ⊤ равносильны (TFAE).

LaTeX

$$$$ \text{TFAE}[IsCoprime(I,J), Codisjoint(I,J), I+J=1, \exists i\in I, \exists j\in J, i+j=1, I \sqcup J = \top] $$$$

Lean4

theorem isCoprime_tfae : TFAE [IsCoprime I J, Codisjoint I J, I + J = 1, ∃ i ∈ I, ∃ j ∈ J, i + j = 1, I ⊔ J = ⊤] :=
  by
  rw [← isCoprime_iff_codisjoint, ← isCoprime_iff_add, ← isCoprime_iff_exists, ← isCoprime_iff_sup_eq]
  simp

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