of_diff

Mathlib.Data.Set.Countable

URI: https://scilib.ai/kg/mathlib#Set.Countable.of_diff

English

If (s \\ t) is countable and t is countable, then s is countable.

Русский

Если s\\t счетно и t счетно, то s счетно.

LaTeX

$$$\\operatorname{Countable}(s \\setminus t) \\wedge \\operatorname{Countable}(t) \\Rightarrow \\operatorname{Countable}(s)$$$

Lean4

theorem of_diff {s t : Set α} (h : (s \ t).Countable) (ht : t.Countable) : s.Countable :=
  (h.union ht).mono (subset_diff_union _ _)

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

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

Разделы

Аффилиация

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