subsingleton_liftStruct_of_mono — Mathlib

English

If p is mono, then LiftStruct sq is a subsingleton.

Русский

Если p моно, то LiftStruct sq — подмножество, содержащее не более одного элемента.

LaTeX

$$$Subsingleton (LiftStruct\ sq)$ under $Mono\ p$$$

Lean4

instance subsingleton_liftStruct_of_mono (sq : CommSq f i p g) [Mono p] : Subsingleton (LiftStruct sq) :=
  ⟨fun l₁ l₂ => by
    ext
    rw [← cancel_mono p]
    simp only [LiftStruct.fac_right]⟩

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