mk_apply — Mathlib

English

The content constructed from the data toFun, monotonicity, and disjoint-sum data, evaluated at K, is exactly toFun(K).

Русский

Содержание, построенное из данных toFun и соответствующих свойств монотонности и суммы по непересекающимся частям, на K равно toFun(K).

LaTeX

$$$\mathrm{mk}(toFun, mono', sup\_disjoint', sup\_le')(K) = toFun(K)$$$

Lean4

@[simp]
theorem mk_apply (toFun : Compacts G → ℝ≥0) (mono' sup_disjoint' sup_le') (K : Compacts G) :
    mk toFun mono' sup_disjoint' sup_le' K = toFun K :=
  rfl

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