exists_forall_ne_zero_of_forall_exists

English

If for each i there exists x with f_i x ≠ 0 for f_i in a family of duals, there exists a single x with f_i x ≠ 0 for all i.

Русский

Если для каждого i существует x, такой что f_i x ≠ 0 в семье двойственных отображений, то существует общий x, для которого f_i x ≠ 0 для всех i.

LaTeX

$$$$ \\exists x, \\forall i, f_i x \\neq 0. $$$$

Lean4

theorem exists_forall_ne_zero_of_forall_exists (f : ι → Dual K M) (h : ∀ i, ∃ x, f i x ≠ 0) : ∃ x, ∀ i, f i x ≠ 0 :=
  by
  let p i := LinearMap.ker (f i)
  replace h i : p i ≠ ⊤ := by specialize h i; aesop
  obtain ⟨x, hx⟩ := Submodule.exists_forall_notMem_of_forall_ne_top p h
  exact ⟨x, by simpa [p] using hx⟩

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