upperClosure_prod — Mathlib

English

upperClosure(s × t) = upperClosure s × upperClosure t for sets s ⊆ α and t ⊆ β.

Русский

upperClosure( s × t ) = upperClosure(s) × upperClosure(t) для множеств s ⊆ α и t ⊆ β.

LaTeX

$$$\\overline{\\mathrm{upper}}(s \\times t) = \\overline{\\mathrm{upper}}(s) \\times \\overline{\\mathrm{upper}}(t)$$$

Lean4

@[simp]
theorem upperClosure_prod (s : Set α) (t : Set β) : upperClosure (s ×ˢ t) = upperClosure s ×ˢ upperClosure t :=
  by
  ext
  simp [Prod.le_def, @and_and_and_comm _ (_ ∈ t)]

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