extensional_of_trichotomous_of_irrefl

English

In a trichotomous irreflexive order, two elements are equal if they have identical sets of predecessors: if for all x, r(x,a) ↔ r(x,b), then a = b.

Русский

В тричотомном иррфлексивном порядке два элемента равны, если их множества предшественников совпадают: ∀x, r(x,a) ↔ r(x,b) ⇒ a = b.

LaTeX

$$$\\\\forall a,b \\\\in \\\\alpha, \\\\ (\\\\forall x, r x a \\\\leftrightarrow r x b) \\\\Rightarrow a = b$$$

Lean4

/-- In a trichotomous irreflexive order, every element is determined by the set of predecessors. -/
theorem extensional_of_trichotomous_of_irrefl (r : α → α → Prop) [IsTrichotomous α r] [IsIrrefl α r] {a b : α}
    (H : ∀ x, r x a ↔ r x b) : a = b :=
  ((@trichotomous _ r _ a b).resolve_left <| mt (H _).2 <| irrefl a).resolve_right <| mt (H _).1 <| irrefl b

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