uIcc_eq_finset_subtype — Mathlib

English

For a,b ∈ ℕ+, the PNats in the closed interval [a, b] correspond exactly to the naturals in [a, b] restricted to positive numbers; i.e. uIcc a b equals (uIcc (a : ℕ) b).subtype (λ n : ℕ, 0 < n).

Русский

Для a,b ∈ ℕ+ PNats в замкнутом интервале [a, b] соответствуют натуральным числам в [a, b], ограниченным положительностью; то есть uIcc a b = (uIcc (a : ℕ) b).subtype (λ n : ℕ, 0 < n).

LaTeX

$$$uIcc(a,b) = (uIcc(a:\\mathbb{N}) b).\\mathrm{subtype}\\ (\\lambda n:\\mathbb{N}, 0

Lean4

theorem uIcc_eq_finset_subtype : uIcc a b = (uIcc (a : ℕ) b).subtype fun n : ℕ => 0 < n :=
  rfl

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