map_cast_heq — Mathlib

English

If α = β via h, then for any Finset s ⊆ α, the image s.map(Equiv.cast h).toEmbedding is heterogeneously equivalent to s.

Русский

Пусть α и β равны по h. Тогда для любого Finset s над α образ s.map(Equiv.cast h).toEmbedding гетерогенно эквивалентен s над β.

LaTeX

$$$HEq( Finset.map(Equiv.cast h).toEmbedding\; s, s)$$$

Lean4

@[simp]
theorem map_cast_heq {α β} (h : α = β) (s : Finset α) : s.map (Equiv.cast h).toEmbedding ≍ s :=
  by
  subst h
  simp

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