embDomain_eq_mapDomain — Mathlib

English

Let f : α ↪ β be an embedding and v ∈ α →₀ M. Then embDomain f v equals mapDomain f v.

Русский

Пусть f : α ↪ β — вложение и v ∈ α →₀ M. Тогда embDomain f v = mapDomain f v.

LaTeX

$$$$ \mathrm{embDomain}\ f\ v = \mathrm{mapDomain}\ f\ v. $$$$

Lean4

theorem embDomain_eq_mapDomain (f : α ↪ β) (v : α →₀ M) : embDomain f v = mapDomain f v :=
  by
  ext a
  by_cases h : a ∈ Set.range f
  · rcases h with ⟨a, rfl⟩
    rw [mapDomain_apply f.injective, embDomain_apply]
  · rw [mapDomain_notin_range, embDomain_notin_range] <;> assumption

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