univ_map_def — Mathlib

English

For an embedding f : Fin n ↪ α, Finset.univ.map f equals ⟨List.ofFn f, List.nodup_ofFn.mpr f.injective⟩.

Русский

Для вложения f : Fin n ↪ α, Finset.univ.map f равно ⟨List.ofFn f, List.nodup_ofFn.mpr f.injective⟩.

LaTeX

$$$\mathrm{Finset.univ}.map f = ⟨\mathrm{List}.ofFn f, \mathrm{List}.nodup\_{\mathrm{ofFn}}(f.injective)\rangle$$$

Lean4

theorem univ_map_def {n : ℕ} (f : Fin n ↪ α) : Finset.univ.map f = ⟨List.ofFn f, List.nodup_ofFn.mpr f.injective⟩ := by
  simp [Finset.map]

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