directed_of₃ — Mathlib

English

Given a directed relation r on α and a,b,c ∈ α, there exists d with r a d, r b d, and r c d.

Русский

Пусть r направлено на α. Для любых a,b,c найдётся d такой, что r a d, r b d и r c d.

LaTeX

$$$\\forall a,b,c \\in α, \\exists d, r a d \\land r b d \\land r c d$$$

Lean4

theorem directed_of₃ (r : α → α → Prop) [IsDirected α r] [IsTrans α r] (a b c : α) : ∃ d, r a d ∧ r b d ∧ r c d :=
  have ⟨e, hae, hbe⟩ := directed_of r a b
  have ⟨f, hef, hcf⟩ := directed_of r e c
  ⟨f, Trans.trans hae hef, Trans.trans hbe hef, hcf⟩

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