range_castLE — Mathlib

English

Same as Range CastLE: if n ≤ k, range of Fin.castLE h is {i ∈ Fin k | i.val < n}.

Русский

То же самое, что и Range CastLE: если n ≤ k, образ Fin.castLE h равен {i ∈ Fin k | i.val < n}.

LaTeX

$$$\\forall {n k : \\mathbb{N}},\\; (n \\le k) \\Rightarrow \\mathrm{Set.range}(\\mathrm{Fin.castLE}\\ h) = \\{ i \\in \\mathrm{Fin}(k) \\mid i.\\mathrm{val} < n \\}$$$

Lean4

@[simp]
theorem range_castLE {n k : ℕ} (h : n ≤ k) : Set.range (castLE h) = {i : Fin k | (i : ℕ) < n} :=
  Set.ext fun x => ⟨fun ⟨y, hy⟩ => hy ▸ y.2, fun hx => ⟨⟨x, hx⟩, rfl⟩⟩

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