euc — Mathlib

English

If x ≃ y and y ≃ z, then x ≃ z.

Русский

Если x эквивалентно y и y эквивалентно z, то x эквивалентно z.

LaTeX

$$∀ {x y z}, Equiv x y → Equiv y z → Equiv x z$$

Lean4

protected theorem euc : ∀ {x y z}, Equiv x y → Equiv z y → Equiv x z
  | ⟨_, _⟩, ⟨_, _⟩, ⟨_, _⟩, ⟨αβ, βα⟩, ⟨γβ, βγ⟩ =>
    ⟨fun a =>
      let ⟨b, ab⟩ := αβ a
      let ⟨c, bc⟩ := βγ b
      ⟨c, Equiv.euc ab bc⟩,
      fun c =>
      let ⟨b, cb⟩ := γβ c
      let ⟨a, ba⟩ := βα b
      ⟨a, Equiv.euc ba cb⟩⟩

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