embDomain_notin_range — Mathlib

English

If a is not in the range of the embedding f, then embDomain f v a = 0.

Русский

Если a не лежит в образе вложения f, то embDomain f v a = 0.

LaTeX

$$embDomain f v a = 0 \\text{ if } a \\notin \\operatorname{range}(f)$$

Lean4

theorem embDomain_notin_range (f : α ↪ β) (v : α →₀ M) (a : β) (h : a ∉ Set.range f) : embDomain f v a = 0 := by
  classical
  refine dif_neg (mt (fun h => ?_) h)
  rcases Finset.mem_map.1 h with ⟨a, _h, rfl⟩
  exact Set.mem_range_self a

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