frontier_prod_univ_eq — Mathlib

English

The boundary (frontier) of a product s × t equals the union of (closure s) × (frontier t) and (frontier s) × (closure t).

Русский

Граница произведения равна объединению (замыкание s)×(грань t) и (грань s)×(замыкание t).

LaTeX

$$$$\mathrm{frontier}(s\times t) = \overline{s}\times\mathrm{frontier}(t) \cup \mathrm{frontier}(s)\times\overline{t}.$$$$

Lean4

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

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