frontier_univ_prod_eq

Mathlib.Topology.Constructions.SumProd

URI: https://scilib.ai/kg/mathlib#frontier_univ_prod_eq

English

Frontier of s × univ equals frontier s × univ.

Русский

Граница s × univ равна frontier(s) × univ.

LaTeX

$$$$\mathrm{frontier}(s\times\mathrm{univ}) = \mathrm{frontier}(s)\times\mathrm{univ}.$$$$

Lean4

@[simp]
theorem frontier_univ_prod_eq (s : Set Y) : frontier ((univ : Set X) ×ˢ s) = univ ×ˢ frontier s := by
  simp [frontier_prod_eq]

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

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

Разделы

Аффилиация

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