English
Let l ∈ α →₀ M, f: α ↪ β, a ∈ β, b ∈ M with b ≠ 0 and l.embDomain f = single a b. Then there exists x ∈ α with l = single x b and f x = a.
Русский
Пусть l ∈ α →₀ M, f: α ↪ β, a ∈ β, b ∈ M, b ≠ 0 и l.embDomain f = single a b. Тогда существует x ∈ α такое, что l = single x b и f x = a.
LaTeX
$$∃ x, l = single x b ∧ f x = a$$
Lean4
theorem single_of_embDomain_single (l : α →₀ M) (f : α ↪ β) (a : β) (b : M) (hb : b ≠ 0)
(h : l.embDomain f = single a b) : ∃ x, l = single x b ∧ f x = a := by
classical
have h_map_support : Finset.map f l.support = { a } := by rw [← support_embDomain, h, support_single_ne_zero _ hb]
have ha : a ∈ Finset.map f l.support := by simp only [h_map_support, Finset.mem_singleton]
rcases Finset.mem_map.1 ha with ⟨c, _hc₁, hc₂⟩
use c
constructor
· ext d
rw [← embDomain_apply f l, h]
by_cases h_cases : c = d
· simp only [Eq.symm h_cases, hc₂, single_eq_same]
· rw [single_apply, single_apply, if_neg, if_neg h_cases]
by_contra hfd
exact h_cases (f.injective (hc₂.trans hfd))
· exact hc₂
