iInf_real_pos_eq_iInf_nnreal_pos — Mathlib

English

For any complete lattice, the infimum taken over all positive real numbers equals the infimum taken over positive nonnegative real numbers.

Русский

Для любой полной решетки несравнимый минимум по всем положительным вещественным числам равен минимума по положительным неотрицательным числам.

LaTeX

$$⨅_{n∈ℝ, n>0} f(n) = ⨅_{n∈ℝ_{≥0}, n>0} f(n)$$

Lean4

theorem iInf_real_pos_eq_iInf_nnreal_pos [CompleteLattice α] {f : ℝ → α} :
    ⨅ (n : ℝ) (_ : 0 < n), f n = ⨅ (n : ℝ≥0) (_ : 0 < n), f n :=
  le_antisymm (iInf_mono' fun r => ⟨r, le_rfl⟩) (iInf₂_mono' fun r hr => ⟨⟨r, hr.le⟩, hr, le_rfl⟩)

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