English
If hchain is a chain on s and a,b,c ∈ s, there exists z ∈ s such that a,b,c are r-related to z pairwise in a transitive fashion.
Русский
Если hchain — цепь на s и a,b,c ∈ s, существует z ∈ s such that a,b,c are related to z by r in a transitive fashion.
LaTeX
$$$ IsChain\\ r\\ s \\rightarrow [IsTrans\\ α\\ r] \\rightarrow \\forall a,b,c \\in s, \\exists z \\in s, r a z \\land r b z \\land r c z $$$
Lean4
theorem exists3 (hchain : IsChain r s) [IsTrans α r] {a b c} (mem1 : a ∈ s) (mem2 : b ∈ s) (mem3 : c ∈ s) :
∃ (z : _) (_ : z ∈ s), r a z ∧ r b z ∧ r c z :=
by
rcases directedOn_iff_directed.mpr (IsChain.directed hchain) a mem1 b mem2 with ⟨z, mem4, H1, H2⟩
rcases directedOn_iff_directed.mpr (IsChain.directed hchain) z mem4 c mem3 with ⟨z', mem5, H3, H4⟩
exact ⟨z', mem5, _root_.trans H1 H3, _root_.trans H2 H3, H4⟩
