closure_one_prod — Mathlib

English

Let s ⊆ M and t ⊆ N with 1 ∈ s. Then closure (s × t) = closure s .prod closure t under the given hypotheses.

Русский

Пусть s ⊆ M и t ⊆ N и 1 ∈ s. Тогда closure(s × t) = closure(s) .prod closure(t) при данных предпосылках.

LaTeX

$$$$ \\operatorname{closure}(s \\times t) = \\operatorname{closure}(s) \\;\\mathrm{prod}\\; \\operatorname{closure}(t) $$$$

Lean4

@[to_additive (attr := simp) closure_zero_prod]
theorem closure_one_prod (t : Set N) : closure (({ 1 } : Set M) ×ˢ t) = .prod ⊥ (closure t) :=
  le_antisymm (closure_le.2 <| Set.prod_subset_prod_iff.2 <| .inl ⟨.rfl, subset_closure⟩)
    (prod_le_iff.2 ⟨by simp, map_le_of_le_comap _ <| closure_le.2 fun _y hy => subset_closure ⟨rfl, hy⟩⟩)

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