card_mono

Mathlib.SetTheory.Cardinal.Finite

URI: https://scilib.ai/kg/mathlib#Nat.card_mono

English

If s ⊆ t and t is finite, Nat.card s ≤ Nat.card t.

Русский

Если s ⊆ t и t конечно, то Nat.card s ≤ Nat.card t.

LaTeX

$$$ (s \subseteq t) \\ \mathrm{Finite}\,t \rightarrow \mathrm{Nat.card}\,s \le \mathrm{Nat.card}\,t $$$

Lean4

theorem card_mono (ht : t.Finite) (h : s ⊆ t) : Nat.card s ≤ Nat.card t :=
  toNat_le_toNat (mk_le_mk_of_subset h) ht.lt_aleph0

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

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

Разделы

Аффилиация

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