some_inter_some

Mathlib.Data.Part

URI: https://scilib.ai/kg/mathlib#Part.some_inter_some

English

some(a) ∩ some(b) equals some(a ∩ b).

Русский

some(a) ∩ some(b) равно some(a ∩ b).

LaTeX

$$$$ \mathrm{some}(a) \cap \mathrm{some}(b) = \mathrm{some}(a \cap b). $$$$

Lean4

theorem some_inter_some [Inter α] (a b : α) : some a ∩ some b = some (a ∩ b) := by simp [inter_def]

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

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

Разделы

Аффилиация

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