comapDomain_add — Mathlib

English

If f is injective and hl ⊆ range f, then mapDomain f (comapDomain f l hf.injOn) = l.

Русский

Если f инъективен и hl ⊆ образ, то mapDomain f (comapDomain f l hf.injOn) = l.

LaTeX

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

Lean4

theorem comapDomain_add (v₁ v₂ : β →₀ M) (hv₁ : Set.InjOn f (f ⁻¹' ↑v₁.support)) (hv₂ : Set.InjOn f (f ⁻¹' ↑v₂.support))
    (hv₁₂ : Set.InjOn f (f ⁻¹' ↑(v₁ + v₂).support)) :
    comapDomain f (v₁ + v₂) hv₁₂ = comapDomain f v₁ hv₁ + comapDomain f v₂ hv₂ :=
  by
  ext
  simp

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