mono

Mathlib.Data.Set.Countable

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

English

If s1 ⊆ s2 and s2 is countable, then s1 is countable.

Русский

Если s1 ⊆ s2 и s2 счётно, то s1 счётно.

LaTeX

$$$\forall s_1 \forall s_2,\ (s_1 \subseteq s_2) \land (s_2.Countable) \implies (s_1.Countable)$$$

Lean4

theorem mono {s₁ s₂ : Set α} (h : s₁ ⊆ s₂) (hs : s₂.Countable) : s₁.Countable :=
  have := hs.to_subtype;
  (inclusion_injective h).countable

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

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

Разделы

Аффилиация

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