ssubset_imp_ssubset

Mathlib.Order.RelClasses

URI: https://scilib.ai/kg/mathlib#GCongr.ssubset_imp_ssubset

English

If c ⊆ a and b ⊆ d and a ⊂ b, then c ⊂ d.

Русский

Если c ⊆ a и b ⊆ d и a ⊂ b, то c ⊂ d.

LaTeX

$$(c \\subseteq a) ∧ (b \\subseteq d) ∧ (a \\subset b) ⇒ c \\subset d$$

Lean4

@[gcongr]
theorem ssubset_imp_ssubset (h₁ : c ⊆ a) (h₂ : b ⊆ d) : a ⊂ b → c ⊂ d := fun h => (h₁.trans_ssubset h).trans_subset h₂

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

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

Разделы

Аффилиация

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