countable_insert — Mathlib

English

The insertion of an element into a set preserves countability: insert a s is countable iff s is countable.

Русский

Добавление элемента в множество сохраняет счетность: insert a s счетно тогда и только тогда, когда s счетно.

LaTeX

$$$\\operatorname{Countable}(\\operatorname{insert}(a,s)) \\iff \\operatorname{Countable}(s)$$$

Lean4

@[simp]
theorem countable_insert {s : Set α} {a : α} : (insert a s).Countable ↔ s.Countable := by
  simp only [insert_eq, countable_union, countable_singleton, true_and]

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