exists_forall_mem_ne_zero_of_forall_exists

English

If for a submodule p and a family f_i of duals there exists x ∈ p with f_i x ≠ 0 for all i, then there exists x ∈ p with all f_i x ≠ 0.

Русский

Если существует x ∈ p, такой что f_i x ≠ 0 для всех i, то существует x ∈ p, для которого f_i x ≠ 0 для всех i.

LaTeX

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

Lean4

/-- A convenience variation of `Module.Dual.exists_forall_ne_zero_of_forall_exists` where we are
concerned only about behaviour on a fixed submodule. -/
theorem exists_forall_mem_ne_zero_of_forall_exists (p : Submodule K M) (f : ι → Dual K M)
    (h : ∀ i, ∃ x ∈ p, f i x ≠ 0) : ∃ x ∈ p, ∀ i, f i x ≠ 0 :=
  by
  let f' (i : ι) : Dual K p := (f i).domRestrict p
  replace h (i : ι) : ∃ x : p, f' i x ≠ 0 := by obtain ⟨x, hxp, hx₀⟩ := h i; exact ⟨⟨x, hxp⟩, hx₀⟩
  obtain ⟨⟨x, hxp⟩, hx₀⟩ := exists_forall_ne_zero_of_forall_exists f' h
  exact ⟨x, hxp, hx₀⟩

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