extendDomain_subtypeDomain — Mathlib

English

Conversely, extending the domain and then restricting back recovers the original function: (subtypeDomain P f).extendDomain = f.

Русский

Обратно: сначала ограничиваем по подтипу, затем расширяем область определения, получаем исходную функцию.

LaTeX

$$$(\\mathrm{subtypeDomain} P f).\\extendDomain = f$$$

Lean4

theorem extendDomain_subtypeDomain (f : α →₀ M) (hf : ∀ a ∈ f.support, P a) : (subtypeDomain P f).extendDomain = f :=
  by
  ext a
  by_cases h : P a
  · exact dif_pos h
  · dsimp [extendDomain_toFun]
    rw [if_neg h, eq_comm, ← notMem_support_iff]
    refine mt ?_ h
    exact hf _

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