ssubset_of_subset_of_ssubset

Mathlib.Data.Set.Basic

URI: https://scilib.ai/kg/mathlib#Set.ssubset_of_subset_of_ssubset

← MathLib Explorer

English

If S1 ⊆ S2 and S2 ⊊ S3, then S1 ⊊ S3.

Русский

Если S1 ⊆ S2 и S2 ⊊ S3, то S1 ⊊ S3.

LaTeX

$$$(s_1 \subseteq s_2) \land (s_2 \subsetneq s_3) \Rightarrow s_1 \subsetneq s_3$$$

Lean4

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

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

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

Разделы

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

Аффилиация

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