exists_mem_carrier_add_eq_zero — Mathlib

English

There exists a pair of elements a ∈ x.carrier and b ∈ y.carrier such that a + b = 0 if and only if x = -y.

Русский

Существует пара элементов a ∈ x.carrier и b ∈ y.carrier такие, что a + b = 0, тогда и только тогда x = −y.

LaTeX

$$$(\\exists a \\in x.carrier)(\\exists b \\in y.carrier), a + b = 0 \\iff x = -y$$$

Lean4

theorem exists_mem_carrier_add_eq_zero (x y : ConjRootClass K L) :
    (∃ᵉ (a ∈ x.carrier) (b ∈ y.carrier), a + b = 0) ↔ x = -y :=
  by
  simp_rw [mem_carrier]
  constructor
  · rintro ⟨a, rfl, b, rfl, h⟩
    rw [mk_neg, mk_eq_mk, add_eq_zero_iff_eq_neg.mp h]
  · rintro rfl
    induction y with
    | h y => exact ⟨-y, mk_neg y, y, rfl, neg_add_cancel _⟩

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