embDomain_comapDomain — Mathlib

English

If hg ensures that the support of g is contained in range f, then embDomain f (comapDomain f g f.injective.injOn) = g.

Русский

Если hg обеспечивает равенство, что поддержка g содержится в образе f, тогда embDomain f (comapDomain f g f.injective.injOn) = g.

LaTeX

$$$$ \embDomain f (\mathrm{comapDomain}\ (f)\ g\ f.injective.injOn) = g $$$$

Lean4

theorem embDomain_comapDomain {f : α ↪ β} {g : β →₀ M} (hg : ↑g.support ⊆ Set.range f) :
    embDomain f (comapDomain f g f.injective.injOn) = g :=
  by
  ext b
  by_cases hb : b ∈ Set.range f
  · obtain ⟨a, rfl⟩ := hb
    rw [embDomain_apply, comapDomain_apply]
  · replace hg : g b = 0 := notMem_support_iff.mp <| mt (hg ·) hb
    rw [embDomain_notin_range _ _ _ hb, hg]

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