compl_mul_closure_one_eq — Mathlib

English

If t · closure({1}) = t, then t^c · closure({1}) = t^c.

Русский

Если $t \\cdot \\overline{\\{1\\}} = t$, то $t^c \\cdot \\overline{\\{1\\}} = t^c$.

LaTeX

$$$t \\cdot \\overline{\\{1\\}} = t \\quad\\Rightarrow\\quad t^{c} \\cdot \\overline{\\{1\\}} = t^{c}$$$

Lean4

@[to_additive]
theorem compl_mul_closure_one_eq {t : Set G} (ht : t * (closure { 1 } : Set G) = t) :
    tᶜ * (closure { 1 } : Set G) = tᶜ :=
  by
  refine Subset.antisymm ?_ (subset_mul_closure_one tᶜ)
  rintro - ⟨x, hx, g, hg, rfl⟩
  by_contra H
  have : x ∈ t * (closure { 1 } : Set G) :=
    by
    rw [← Subgroup.coe_topologicalClosure_bot G] at hg ⊢
    simp only [mem_compl_iff, not_not] at H
    exact ⟨x * g, H, g⁻¹, Subgroup.inv_mem _ hg, by simp⟩
  rw [ht] at this
  exact hx this

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