lowerClosure_prod — Mathlib

English

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

Русский

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

LaTeX

$$$\\underline{\\mathrm{lower}}(s \\times t) = \\underline{\\mathrm{lower}}(s) \\times \\underline{\\mathrm{lower}}(t)$$$

Lean4

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

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