image_commutatorSet_closureCommutatorRepresentatives

English

The image of commutatorSet under the subtype inclusion equals commutatorSet(G): image(commutatorSet(G)) = commutatorSet(G).

Русский

Образ commutatorSet(G) при включении подпредставления равен commutatorSet(G).

LaTeX

$$$ (\\text{closureCommutatorRepresentatives}(G)).subtype'' commutatorSet (closureCommutatorRepresentatives(G)) = commutatorSet(G) $$$

Lean4

theorem image_commutatorSet_closureCommutatorRepresentatives :
    (closureCommutatorRepresentatives G).subtype '' commutatorSet (closureCommutatorRepresentatives G) =
      commutatorSet G :=
  by
  apply Set.Subset.antisymm
  · rintro - ⟨-, ⟨g₁, g₂, rfl⟩, rfl⟩
    exact ⟨g₁, g₂, rfl⟩
  ·
    exact fun g hg ↦
      ⟨_,
        ⟨⟨_, subset_closure <| .inl ⟨_, ⟨⟨g, hg⟩, rfl⟩, rfl⟩⟩, ⟨_, subset_closure <| .inr ⟨_, ⟨⟨g, hg⟩, rfl⟩, rfl⟩⟩,
          rfl⟩,
        hg.choose_spec.choose_spec⟩

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