isClosed_centralizer — Mathlib

English

In a Hausdorff magma with continuous multiplication, the centralizer of any set is closed.

Русский

В несмещенной магме с непрерывным умножением центральизатор любого множества замкнут.

LaTeX

$$$IsClosed(centralizer(s))$$$

Lean4

/-- In a Hausdorff magma with continuous multiplication, the centralizer of any set is closed. -/
theorem isClosed_centralizer {M : Type*} (s : Set M) [Mul M] [TopologicalSpace M] [ContinuousMul M] [T2Space M] :
    IsClosed (centralizer s) := by
  rw [centralizer, setOf_forall]
  refine isClosed_sInter ?_
  rintro - ⟨m, ht, rfl⟩
  refine isClosed_imp (by simp) <| isClosed_eq ?_ ?_
  all_goals fun_prop

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