multiplicativeClosure_le_iff — Mathlib

English

The map taking a morphism property to its multiplicative closure is monotone.

Русский

Отображение, отправляющее свойство морфизмов в его замыкание по умножению, монотонно.

LaTeX

$$$\mathrm{Monotone}(\mathrm{multiplicativeClosure})$$$

Lean4

/-- The multiplicative closure of `W` is the smallest multiplicative property greater than or equal
to `W`. -/
@[simp]
theorem multiplicativeClosure_le_iff (W' : MorphismProperty C) [W'.IsMultiplicative] :
    multiplicativeClosure W ≤ W' ↔ W ≤ W'
    where
  mp h := le_multiplicativeClosure W |>.trans h
  mpr
    h := by
    intro _ _ _ hf
    induction hf with
    | of _ hf => exact h _ hf
    | id x => exact W'.id_mem _
    | comp_of _ _ _ hg hf => exact W'.comp_mem _ _ hf (h _ hg)

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