closure_prod_one — Mathlib

English

The symmetric form of the previous result: for appropriate s,t, closure(s × t) = closure(s) .prod closure(t).

Русский

Симметричная форма предыдущего утверждения: для подходящих s, t выполняется 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_prod_zero]
theorem closure_prod_one (s : Set M) : closure (s ×ˢ ({ 1 } : Set N)) = (closure s).prod ⊥ :=
  le_antisymm (closure_le.2 <| Set.prod_subset_prod_iff.2 <| .inl ⟨subset_closure, .rfl⟩)
    (prod_le_iff.2 ⟨map_le_of_le_comap _ <| closure_le.2 fun _x hx => subset_closure ⟨hx, rfl⟩, by simp⟩)

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