liftContinuousCommMonoidHom_mk — Mathlib

English

The lift of a continuous monoid hom f : M → N to SeparationQuotient M → N exists provided hf holds that inseparable x y implies f x = f y.

Русский

Существует подъем непрерывного моноидного гомоморфизма f: M → N на SeparationQuotient M → N, если hf обеспечивает равенство на inseparable.

LaTeX

$$$\mathrm{liftContinuousMonoidHom}:\; (f: \mathrm{ContinuousMonoidHom}\ M\ N) \to (\mathrm{SeparationQuotient}\ M \to_L[N] N)$$$

Lean4

@[to_additive (attr := simp)]
theorem liftContinuousCommMonoidHom_mk [CommMonoid M] [ContinuousMul M] [CommMonoid N] (f : ContinuousMonoidHom M N)
    (hf : ∀ x y, Inseparable x y → f x = f y) (x : M) : liftContinuousMonoidHom f hf (mk x) = f x :=
  rfl

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