ssubset_of_ssubset_of_subset

Mathlib.Data.Set.Basic

URI: https://scilib.ai/kg/mathlib#Set.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 \subsetneq s_2) \land (s_2 \subseteq s_3) \Rightarrow s_1 \subsetneq s_3$$$

Lean4

protected theorem ssubset_of_ssubset_of_subset {s₁ s₂ s₃ : Set α} (hs₁s₂ : s₁ ⊂ s₂) (hs₂s₃ : s₂ ⊆ s₃) : s₁ ⊂ s₃ :=
  ⟨Subset.trans hs₁s₂.1 hs₂s₃, fun hs₃s₁ => hs₁s₂.2 (Subset.trans hs₂s₃ hs₃s₁)⟩

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

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

Разделы

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

Аффилиация

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