t2Space_of_one_sep — Mathlib

English

If t is closed and s is compact, then instHMul.hMul t s is closed.

Русский

Если t замкнуто и s компактно, то произведение t · s замкнуто.

LaTeX

$$$\\forall S,T \\subseteq G,\\ (\\text{IsClosed}(T) \\wedge \\text{IsCompact}(S)) \\Rightarrow \\text{IsClosed}(\\operatorname{hMul}(T,S))$$$

Lean4

@[to_additive]
theorem t2Space_of_one_sep (H : ∀ x : G, x ≠ 1 → ∃ U ∈ 𝓝 (1 : G), x ∉ U) : T2Space G :=
  by
  suffices T1Space G from inferInstance
  refine t1Space_iff_specializes_imp_eq.2 fun x y hspec ↦ by_contra fun hne ↦ ?_
  rcases H (x * y⁻¹) (by rwa [Ne, mul_inv_eq_one]) with ⟨U, hU₁, hU⟩
  exact hU <| mem_of_mem_nhds <| hspec.map (continuous_mul_right y⁻¹) (by rwa [mul_inv_cancel])

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