codisjoint_iff_exists_add_eq — Mathlib

English

Codisjoint p p' holds iff for every z ∈ M there exist x ∈ p and y ∈ p' with x+y=z.

Русский

Codisjoint p p' выполняется тогда, когда для каждого z ∈ M найдутся x ∈ p и y ∈ p' такие, что x+y=z.

LaTeX

$$$$ Codisjoint\\ p\\ p' \\iff \\forall z \\in M, \\exists x \\in p, \\exists y \\in p', x+y=z. $$$$

Lean4

theorem codisjoint_iff_exists_add_eq : Codisjoint p p' ↔ ∀ z, ∃ x y, x ∈ p ∧ y ∈ p' ∧ x + y = z :=
  by
  rw [codisjoint_iff, eq_top_iff']
  exact forall_congr' (fun z => mem_sup.trans <| by simp)

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