existsUnique_add_of_isCompl — Mathlib

English

There exists a unique decomposition of x into p- and q-components, with an explicit uniqueness condition.

Русский

Существуют уникальные p- и q-компоненты разложения x с явными условиями уникальности.

LaTeX

$$$\exists!\; u\in p, v\in q:\; (u:E)+v=x$$$

Lean4

theorem existsUnique_add_of_isCompl (hc : IsCompl p q) (x : E) :
    ∃ (u : p) (v : q), (u : E) + v = x ∧ ∀ (r : p) (s : q), (r : E) + s = x → r = u ∧ s = v :=
  let ⟨u, hu₁, hu₂⟩ := existsUnique_add_of_isCompl_prod hc x
  ⟨u.1, u.2, hu₁, fun r s hrs => Prod.eq_iff_fst_eq_snd_eq.1 (hu₂ ⟨r, s⟩ hrs)⟩

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