mapDomain_comapDomain — Mathlib

English

Same as 96432: under injOn and hl ⊆ range f, mapDomain f (comapDomain f l hf.injOn) = l.

Русский

То же самое, что и 96432: при условии injOn и hl ⊆ образ, mapDomain f (comapDomain f l hf.injOn) = l.

LaTeX

$$$$ mapDomain\ f\ (comapDomain f l hf.injOn) = l. $$$$

Lean4

theorem mapDomain_comapDomain (hf : Function.Injective f) (l : β →₀ M) (hl : ↑l.support ⊆ Set.range f) :
    mapDomain f (comapDomain f l hf.injOn) = l :=
  by
  conv_rhs => rw [← embDomain_comapDomain (f := ⟨f, hf⟩) hl (M := M), embDomain_eq_mapDomain]
  rfl

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