ssubset_of_ssubset_of_subset

Mathlib.Data.Finset.Defs

URI: https://scilib.ai/kg/mathlib#Finset.ssubset_of_ssubset_of_subset

← MathLib Explorer

English

If s1 ⊂ s2 and s2 ⊆ s3, then s1 ⊂ s3.

Русский

Если s1 ⊂ s2 и s2 ⊆ s3, то s1 ⊂ s3.

LaTeX

$$$s_1 \subset s_2 \land s_2 \subseteq s_3 \Rightarrow s_1 \subset s_3$$$

Lean4

theorem ssubset_of_ssubset_of_subset {s₁ s₂ s₃ : Finset α} (hs₁s₂ : s₁ ⊂ s₂) (hs₂s₃ : s₂ ⊆ s₃) : s₁ ⊂ s₃ :=
  Set.ssubset_of_ssubset_of_subset hs₁s₂ hs₂s₃

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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