subset_interior_mul_left — Mathlib

English

A surjective homomorphism of topological groups is open when the source is sigma-compact and the target is a Baire space.

Русский

Сюръективный гомоморфизм топологических групп открыт, если источник σ-компактен, а цель — пространство Баири.

LaTeX

$$$\\forall f:\\, G \\to H\\text{ morphism with } Surjective(f) \\wedge \\Sigma-Compact(G) \\wedge \\text{Baire}(H) \\Rightarrow IsOpenMap(f).$$$

Lean4

@[to_additive]
theorem subset_interior_mul_left : interior s * t ⊆ interior (s * t) :=
  interior_maximal (Set.mul_subset_mul_right interior_subset) isOpen_interior.mul_right

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