subset_interior_smul — Mathlib

English

The product of the interiors of two sets under a group action contains the interior of their product: interior s • interior t ⊆ interior(s • t).

Русский

Произведение interior s и interior t по действию группы содержит interior(s · t).

LaTeX

$$$\\operatorname{Int}(s) \\cdot \\operatorname{Int}(t) \\subseteq \\operatorname{Int}(s\\cdot t).$$$

Lean4

@[to_additive]
theorem subset_interior_smul : interior s • interior t ⊆ interior (s • t) :=
  (Set.smul_subset_smul_right interior_subset).trans subset_interior_smul_right

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