inter_subset_inter

Mathlib.Data.Finset.Lattice.Basic

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

English

If x ⊆ y and s ⊆ t, then x ∩ s ⊆ y ∩ t.

Русский

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

LaTeX

$$$ x \cap s \subseteq y \cap t $$$

Lean4

@[mono, gcongr]
theorem inter_subset_inter {x y s t : Finset α} (h : x ⊆ y) (h' : s ⊆ t) : x ∩ s ⊆ y ∩ t := by grind

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

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

Разделы

Аффилиация

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