mul_inf_assoc — Mathlib

English

Let A,B,C be subgroups with C ≤ A. Then (A ∩ B) C = A ∩ (B C) as sets.

Русский

Пусть A,B,C — подгруппы, C ≤ A. Тогда (A ∩ B) C = A ∩ (B C) как множества.

LaTeX

$$$(A\\cap B)\\,C = A\\cap (B C)\\quad\\text{if } C\\le A,$$$

Lean4

@[to_additive]
theorem mul_inf_assoc (A B C : Subgroup G) (h : A ≤ C) : (A : Set G) * ↑(B ⊓ C) = (A : Set G) * (B : Set G) ∩ C :=
  by
  ext
  simp only [coe_inf, Set.mem_mul, Set.mem_inter_iff]
  constructor
  · rintro ⟨y, hy, z, ⟨hzB, hzC⟩, rfl⟩
    refine ⟨?_, mul_mem (h hy) hzC⟩
    exact ⟨y, hy, z, hzB, rfl⟩
  rintro ⟨⟨y, hy, z, hz, rfl⟩, hyz⟩
  refine ⟨y, hy, z, ⟨hz, ?_⟩, rfl⟩
  suffices y⁻¹ * (y * z) ∈ C by simpa
  exact mul_mem (inv_mem (h hy)) hyz

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