exists_eq_one_ne_zero_of_ne_zero_pair

English

Let x,y ∈ V with x ≠ 0 and y ≠ 0. Then there exists a functional f in StrongDual 𝕜 V with f(x) = 1 and f(y) ≠ 0.

Русский

Пусть x,y ∈ V и x ≠ 0, y ≠ 0. Существут функционал f ∈ StrongDual 𝕜 V такой, что f(x) = 1 и f(y) ≠ 0.

LaTeX

$$$\exists f \in StrongDual 𝕜 V, f(x) = 1 \land f(y) \neq 0$$$

Lean4

theorem exists_eq_one_ne_zero_of_ne_zero_pair {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) :
    ∃ f : StrongDual R V, f x = 1 ∧ f y ≠ 0 :=
  by
  obtain ⟨u, ux⟩ : ∃ u : StrongDual R V, u x = 1 := exists_eq_one hx
  rcases ne_or_eq (u y) 0 with uy | uy
  · exact ⟨u, ux, uy⟩
  obtain ⟨v, vy⟩ : ∃ v : StrongDual R V, v y = 1 := exists_eq_one hy
  rcases ne_or_eq (v x) 0 with vx | vx
  · exact ⟨(v x)⁻¹ • v, inv_mul_cancel₀ vx, show (v x)⁻¹ * v y ≠ 0 by simp [vx, vy]⟩
  · exact ⟨u + v, by simp [ux, vx], by simp [uy, vy]⟩

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