toOpens_inf — Mathlib

English

In the additive setting, the infimum of OpenAddSubgroups U and V corresponds to the intersection of their opens: (↑(U ⊓ V) : Opens G) = ↑U ∩ ↑V.

Русский

В аддитивном случае пересечение открытых подподгрупп OpenAddSubgroup соответствует пересечению их открытых множеств.

LaTeX

$$$$(U \\wedge V)^{\\mathrm{Opens}} = U^{\\mathrm{Opens}} \\cap V^{\\mathrm{Opens}}.$$$$

Lean4

@[to_additive (attr := simp, norm_cast)]
theorem toOpens_inf : (↑(U ⊓ V) : Opens G) = ↑U ⊓ ↑V :=
  rfl

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