mul_eq_zero_add_eq_one_ext_left — Mathlib

English

Let a and b be elements of the subtype of pairs (x,y) with x,y ∈ R and xy = 0, x+y = 1. Then equality of a and b is determined by the equality of their first components; in particular, if a_1 = b_1, then a = b.

Русский

Пусть a и b — элементы подтипа пар (x,y) таких, что x y = 0 и x + y = 1. Тогда равенство a и b определяется равенством их первых компонент; если a_1 = b_1, то a = b.

LaTeX

$$Let A = { (x,y) ∈ R × R : x y = 0 ∧ x + y = 1 }. Then for all a,b ∈ A, a_1 = b_1 ⇒ a = b.$$

Lean4

theorem mul_eq_zero_add_eq_one_ext_left (eq : a.1.1 = b.1.1) : a = b :=
  by
  refine Subtype.ext <| Prod.ext_iff.mpr ⟨eq, eq_of_mul_eq_add_eq_one a.1.1 ?_ a.2.2 ?_⟩
  · rw [a.2.1, mul_comm, eq, b.2.1]
  · rw [eq, b.2.2]

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