map_univ_val_equiv — Mathlib

English

For any equivalence e: α ≃ β, map e on univ.val equals univ.val.

Русский

Для любого эквивалента e: α ≃ β отображение map e на univ.val равно univ.val.

LaTeX

$$$$ \\operatorname{map} \\, e \; \\operatorname{univ}.\\operatorname{val} = \\operatorname{univ}.\\operatorname{val}. $$$$

Lean4

@[simp]
theorem map_univ_val_equiv (e : α ≃ β) : map e univ.val = univ.val := by
  rw [← congr_arg Finset.val (Finset.map_univ_equiv e), Finset.map_val, Equiv.coe_toEmbedding]

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