instIsPretransitiveOfSubsingleton

English

If α is a subsingleton and M acts on α, then the action is pretransitive: for any x,y in α there exists m ∈ M with m•x = y (take x=y).

Русский

Если α — singleton и действует на него моноид M, тогда действие предпереставимо: для любых x,y∈α существует m∈M такое, что m•x = y (возьмём x=y).

LaTeX

$$$\\text{Subsingleton}(\\alpha) \\implies \\text{MulAction.IsPretransitive } M \\alpha$; в частности, для любых x,y найдём m=1 с x=y.$$

Lean4

@[to_additive]
instance instIsPretransitiveOfSubsingleton {M α : Type*} [Monoid M] [MulAction M α] [Subsingleton α] :
    MulAction.IsPretransitive M α where exists_smul_eq x y := ⟨1, by simp only [one_smul, Subsingleton.elim x y]⟩

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