frontier_prod_eq — Mathlib

English

Simplified relations for membership in the product of closures and related sets.

Русский

Упрощения для принадлежности в произведении замыканий и связанных множеств.

LaTeX

$$$$\text{Simplified relations between }\overline{s\times t},\overline{s},\overline{t}. $$$$

Lean4

theorem frontier_prod_eq (s : Set X) (t : Set Y) :
    frontier (s ×ˢ t) = closure s ×ˢ frontier t ∪ frontier s ×ˢ closure t := by
  simp only [frontier, closure_prod_eq, interior_prod_eq, prod_diff_prod]

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