coe_attachFin — Mathlib

English

As sets, attachFin corresponds to the preimage of s under the natural valuation map; i.e., the underlying set of attachFin equals Fin.val preimage of s.

Русский

Как множества, attachFin равен прообразу под отображением пронумерации элементов, т.е. множество-основание attachFin совпадает с Fin.val^{-1}(s).

LaTeX

$$(attachFin s h)^{\\uparrow} = Fin.val^{-1} s.toSet$$

Lean4

@[simp]
theorem coe_attachFin {s : Finset ℕ} (h : ∀ m ∈ s, m < n) : (attachFin s h : Set (Fin n)) = Fin.val ⁻¹' s := by ext;
  simp

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