card_prod_singleton

Mathlib.SetTheory.Cardinal.Finite

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

← MathLib Explorer

English

For any set s ⊆ α and b ∈ β, Nat.card(s ×ˢ {b}) = Nat.card s.

Русский

Для любого множества s ⊆ α и b ∈ β, Nat.card(s ×ˢ {b}) = Nat.card s.

LaTeX

$$$$ Nat.card\left(s \timesˢ \{b\}\right) = Nat.card(s) $$$$

Lean4

theorem card_prod_singleton (s : Set α) (b : β) : Nat.card (s ×ˢ { b }) = Nat.card s := by
  rw [prod_singleton, Nat.card_image_of_injective (Prod.mk_left_injective b)]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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