English
If a family of linear maps L_i has kernels whose infimum lies in the kernel of K, then K lies in the span of the ranges of L.
Русский
Если семейство отображений L_i имеет общую ямку пересечения (iInf ker L_i) ≤ ker K, то K лежит в линейном замке диапазонов L_i.
LaTeX
$$iInf ker (L i) ≤ ker (K) → K ∈ span range(L)$$
Lean4
/-- Consider a reflexive module and a set `s` of linear forms. If for any `z ≠ 0` there exists
`f ∈ s` such that `f z ≠ 0`, then `s` spans the whole dual space. -/
theorem span_eq_top_of_ne_zero [IsReflexive R M] {s : Set (M →ₗ[R] R)} [Free R ((M →ₗ[R] R) ⧸ (span R s))]
(h : ∀ z ≠ 0, ∃ f ∈ s, f z ≠ 0) : span R s = ⊤ :=
by
by_contra! hn
obtain ⟨φ, φne, hφ⟩ := exists_dual_map_eq_bot_of_lt_top hn.lt_top inferInstance
let φs := (evalEquiv R M).symm φ
have this f (hf : f ∈ s) : f φs = 0 := by
rw [← mem_bot R, ← hφ, mem_map]
exact ⟨f, subset_span hf, (apply_evalEquiv_symm_apply R M f φ).symm⟩
obtain ⟨x, xs, hx⟩ := h φs (by simp [φne, φs])
exact hx <| this x xs
