coe_inf — Mathlib

English

The set corresponding to the infimum of two open subgroups, viewed as Opens, is the intersection of the two open sets: (U ⊓ V)^{Opens} = U^{Opens} ∩ V^{Opens}.

Русский

Множество, соответствующее пересечению двух открытых подгрупп, как открытое множество, есть пересечение двух открытых множеств: (U ⊓ V)^{Opens} = U^{Opens} ∩ V^{Opens}.

LaTeX

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

Lean4

@[to_additive (attr := simp, norm_cast)]
theorem coe_inf : (↑(U ⊓ V) : Set G) = (U : Set G) ∩ V :=
  rfl

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