ssubset_of_subset_of_ssubset

Mathlib.Data.Finset.Defs

URI: https://scilib.ai/kg/mathlib#Finset.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 \to s_2 \subset s_3 \Rightarrow s_1 \subset s_3$$$

Lean4

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

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

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

Разделы

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

Аффилиация

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