encard_congr

Mathlib.Data.Set.Card

URI: https://scilib.ai/kg/mathlib#Set.encard_congr

English

The encard of a set is invariant under a bijection between the underlying sets: if s is equivalent to t, then s.encard = t.encard.

Русский

Энкарда множества не меняется при биекции между его элементами: если s эквивалентно t, то s.encard = t.encard.

LaTeX

$$$ s.encard = t.encard $$$

Lean4

theorem encard_congr (e : s ≃ t) : s.encard = t.encard :=
  ENat.card_congr e

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

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

Разделы

Аффилиация

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