lsubtypeDomain_apply — Mathlib

English

For any f ∈ α →₀ M, applying lsubtypeDomain s to f equals applying subtypeDomain to f with predicate x ∈ s. The two definitions coincide as functions.

Русский

Для любого f ∈ α →₀ M применение lsubtypeDomain s к f равно применению subtypeDomain к f с предикатом x ∈ s. Эти определения совпадают как функции.

LaTeX

$$$(lsubtypeDomain\,s : (α→₀ M) \\to_\\ell[R] s→₀ M)\\;f = \\mathrm{subtypeDomain}(\\lambda x. x∈s)\\;f$$$

Lean4

theorem lsubtypeDomain_apply (f : α →₀ M) :
    (lsubtypeDomain s : (α →₀ M) →ₗ[R] s →₀ M) f = subtypeDomain (fun x => x ∈ s) f :=
  rfl

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