mono

Mathlib.Data.Finset.Slice

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

English

If A ⊆ B and B is sized r, then A is sized r as well.

Русский

Если A ⊆ B и B имеет размер r, то и A имеет размер r.

LaTeX

$$$$ A \subseteq B \quad \Longrightarrow \quad A.Sized r \Rightarrow B.Sized r \Rightarrow A.Sized r $$$$

Lean4

theorem mono (h : A ⊆ B) (hB : B.Sized r) : A.Sized r := fun _x hx => hB <| h hx

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

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

Разделы

Аффилиация

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