inf_normalizer_le_normalizer_inf — Mathlib

English

The infimum of the normalizers of H and K equals the normalizer of H ∩ K.

Русский

Наименьшее верхнее/нижнее нормализаторов удовлетворяет: нормализатор(H) ∩ нормализатор(K) ≤ нормализатор(H ∩ K).

LaTeX

$$$\mathrm{normalizer}(H) \wedge \mathrm{normalizer}(K) \le \mathrm{normalizer}(H \cap K)$$$

Lean4

@[to_additive]
theorem inf_normalizer_le_normalizer_inf : H.normalizer ⊓ K.normalizer ≤ (H ⊓ K).normalizer := fun _ h g ↦
  and_congr (h.1 g) (h.2 g)

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