expGrowthInfTopHom — Mathlib

English

For a finite set s, expGrowthInf( ⨅ x ∈ s, u x ) = ⨅ x ∈ s, expGrowthInf(u x).

Русский

Для конечного множества s: expGrowthInf( ⨅ x ∈ s, u x ) = ⨅ x ∈ s, expGrowthInf(u x).

LaTeX

$$$\expGrowthInf\left(\bigwedge_{x \in s} u_x\right) = \bigwedge_{x \in s} \expGrowthInf(u_x)$$$

Lean4

/-- Lower exponential growth as an `InfTopHom`. -/
noncomputable def expGrowthInfTopHom : InfTopHom (ℕ → ℝ≥0∞) EReal
    where
  toFun := expGrowthInf
  map_inf' _ _ := expGrowthInf_inf
  map_top' := expGrowthInf_top

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