inter_subset_inter

Mathlib.Data.Set.Basic

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

English

If s1 ⊆ t1 and s2 ⊆ t2 then s1 ∩ s2 ⊆ t1 ∩ t2.

Русский

Если s1 ⊆ t1 и s2 ⊆ t2, то s1 ∩ s2 ⊆ t1 ∩ t2.

LaTeX

$$(s1 \subseteq t1) \land (s2 \subseteq t2) \Rightarrow s1 \cap s2 \subseteq t1 \cap t2$$

Lean4

@[gcongr]
theorem inter_subset_inter {s₁ s₂ t₁ t₂ : Set α} (h₁ : s₁ ⊆ t₁) (h₂ : s₂ ⊆ t₂) : s₁ ∩ s₂ ⊆ t₁ ∩ t₂ := fun _ =>
  And.imp (@h₁ _) (@h₂ _)

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

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

Разделы

Аффилиация

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