instInf — Mathlib

English

There is a Min (CompactlySupportedContinuousMap α β) instance, i.e., C_c(α,β) has a infimum operation defined pointwise via β with compact support preserved.

Русский

Существует инстанс Inf для C_c(α,β): есть операция Inf, задаваемая точечно через Inf β и сохраняющая компактную опору.

LaTeX

$$Min (C_c(α,β))$$

Lean4

instance instInf : Min C_c(α, β) where
  min f
    g :=
    { toFun := f ⊓ g
      continuous_toFun := Continuous.inf f.continuous g.continuous
      hasCompactSupport' := f.hasCompactSupport.inf g.hasCompactSupport }

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