ssuperset_imp_ssuperset

Mathlib.Order.RelClasses

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

English

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

Русский

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

LaTeX

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

Lean4

@[gcongr]
theorem ssuperset_imp_ssuperset (h₁ : a ⊆ c) (h₂ : d ⊆ b) : a ⊃ b → c ⊃ d :=
  ssubset_imp_ssubset h₂ h₁

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

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

Разделы

Аффилиация

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