raise'Finset — Mathlib

English

The sequence raise' l n can be turned into a finite set; elements are distinct thanks to raise'_sorted.

Русский

Последовательность raise' l n может быть превращена в конечное множество; элементы различны благодаря raise'_sorted.

LaTeX

$$$\text{raise' Finset}(l,n) = \text{Finset of } \text{raise'}(l,n) \text{ with distinct elements by } \text{raise'}_\text{sorted}$$$

Lean4

/-- Makes `raise' l n` into a finset. Elements are distinct thanks to `raise'_sorted`. -/
def raise'Finset (l : List ℕ) (n : ℕ) : Finset ℕ :=
  ⟨raise' l n, (raise'_sorted _ _).imp (@ne_of_lt _ _)⟩

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