mk_preimage_equiv

Mathlib.SetTheory.Cardinal.Basic

URI: https://scilib.ai/kg/mathlib#Cardinal.mk_preimage_equiv

English

For any bijection f: α ≃ β and any set s ⊆ β, |f^{-1}(s)| = |s|.

Русский

Для любой биекции f: α ≃ β и любого множества s ⊆ β выполняется |f^{-1}(s)| = |s|.

LaTeX

$$$#(f^{-1}' s) = #s$$$

Lean4

@[simp]
theorem mk_preimage_equiv (f : α ≃ β) (s : Set β) : #(f ⁻¹' s) = #s := by simpa using mk_preimage_equiv_lift f s

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru