linearGrowthInf_inf — Mathlib

English

The infimum of the pointwise minimum equals the minimum of infima: linearGrowthInf(u ⊓ v) = min(linearGrowthInf u, linearGrowthInf v).

Русский

Инфинум по точечному минимуму равен минимуму инфимумов: linearGrowthInf(u ⊓ v) = min(linearGrowthInf u, linearGrowthInf v).

LaTeX

$$$\operatorname{linearGrowthInf}(u \sqcap v) = \min\bigl( \operatorname{linearGrowthInf}(u), \operatorname{linearGrowthInf}(v) \bigr)$$$

Lean4

theorem linearGrowthInf_inf : linearGrowthInf (u ⊓ v) = min (linearGrowthInf u) (linearGrowthInf v) :=
  by
  rw [linearGrowthInf, linearGrowthInf, linearGrowthInf, ← liminf_min]
  refine liminf_congr (Eventually.of_forall fun n ↦ ?_)
  exact (monotone_div_right_of_nonneg n.cast_nonneg').map_min

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