coe_mul_of_right_le_normalizer_left

English

If H ≤ N.normalizer, then the carrier of N ⊔ H equals N H.

Русский

Пусть H ≤ N.normalizer. Тогда носитель N ⊔ H равен N H.

LaTeX

$$$\\uparrow (N\\lor H) = N H$$$

Lean4

/-- The carrier of `N ⊔ H` is just `↑N * ↑H` (pointwise set product) when
`H` is a subgroup of the normalizer of `N` in `G`. -/
@[to_additive /-- The carrier of `N ⊔ H` is just `↑N + ↑H` (pointwise set addition)
    when `H` is a subgroup of the normalizer of `N` in `G`. -/
    ]
theorem coe_mul_of_right_le_normalizer_left (N H : Subgroup G) (hLE : H ≤ N.normalizer) : (↑(N ⊔ H) : Set G) = N * H :=
  by rw [← set_mul_normalizer_comm _ _ hLE, sup_comm, coe_mul_of_left_le_normalizer_right _ _ hLE]

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