memHolder_const' — Mathlib

English

MemHolder r f holds for a constant function: MemHolder r (Function.const X c).

Русский

MemHolder r f выполняется для константной функции: MemHolder r (Function.const X c).

LaTeX

$$$\operatorname{MemHolder}(r,\mathrm{const}_X c).$$$

Lean4

/-- Version of `memHolder_const` with the spelling `fun _ ↦ c` for the constant function. -/
@[simp]
theorem memHolder_const' {c : Y} : MemHolder r (fun _ ↦ c : X → Y) :=
  memHolder_const

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