inter_pow_subset

Mathlib.Algebra.Group.Pointwise.Finset.Basic

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

English

The nth power of the intersection is contained in the intersection of nth powers: (s ∩ t)^n ⊆ s^n ∩ t^n.

Русский

Произведение пересечения по степени n содержится в пересечении степеней: (s ∩ t)^n ⊆ s^n ∩ t^n.

LaTeX

$$$ (s \\cap t)^n \\subseteq s^n \\cap t^n $$$

Lean4

@[to_additive]
theorem inter_pow_subset : (s ∩ t) ^ n ⊆ s ^ n ∩ t ^ n := by apply subset_inter <;> gcongr <;> simp

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

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

Разделы

Аффилиация

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