multiplicativeClosure_eq_multiplicativeClosure'

English

The multiplicative closure of W equals the multiplicativeClosure' of W.

Русский

Замыкание по умножению W равно multiplicativeClosure' W.

LaTeX

$$$W.multiplicativeClosure = W.multiplicativeClosure'$$$

Lean4

theorem multiplicativeClosure_eq_multiplicativeClosure' : W.multiplicativeClosure = W.multiplicativeClosure' :=
  le_antisymm ((multiplicativeClosure_le_iff _ _).mpr (fun _ _ f hf ↦ .of f hf)) <| fun x y f hf ↦ by
    induction hf with
    | of _ h => exact .of _ h
    | id x => exact .id x
    | of_comp f g hf hg hr => exact W.multiplicativeClosure.comp_mem f g (.of f hf) hr

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