isLink_iff_eq — Mathlib

English

If h: G.IsLink e x y, then for any z, G.IsLink e x z holds if and only if z = y.

Русский

Если h: IsLink e x y, то для любого z IsLink e x z выполняется тогда и только тогда, когда z = y.

LaTeX

$$$\\text{IsLink}(G,e,x,y) \\Rightarrow (\\forall z, \\text{IsLink}(G,e,x,z) \\iff z = y).$$$

Lean4

theorem isLink_iff_eq (h : G.IsLink e x y) : G.IsLink e x z ↔ z = y :=
  ⟨fun h' ↦ h'.right_unique h, fun h' ↦ h' ▸ h⟩

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