subset_inter

Mathlib.Data.Set.Basic

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

English

If r ⊆ s and r ⊆ t, then r ⊆ s ∩ t.

Русский

Если r ⊆ s и r ⊆ t, то r ⊆ s ∩ t.

LaTeX

$$$r \subseteq s \land r \subseteq t \Rightarrow r \subseteq s \cap t$$$

Lean4

theorem subset_inter {s t r : Set α} (rs : r ⊆ s) (rt : r ⊆ t) : r ⊆ s ∩ t := fun _ h => ⟨rs h, rt h⟩

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

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

Разделы

Аффилиация

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