inter_subset_right

Mathlib.Data.Finset.Lattice.Basic

URI: https://scilib.ai/kg/mathlib#Finset.inter_subset_right

English

The intersection is contained in the right operand: s1 ∩ s2 ⊆ s2.

Русский

Пересечение содержится в правом аргументе: s1 ∩ s2 ⊆ s2.

LaTeX

$$$s_{1} \\cap s_{2} \\subseteq s_{2}$$$

Lean4

@[simp]
theorem inter_subset_right : s₁ ∩ s₂ ⊆ s₂ := fun _ ↦ mem_of_mem_inter_right

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

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

Разделы

Аффилиация

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