trans — Mathlib

English

If r is transitive, then the inverse image relation via any function f is transitive.

Русский

Если r транзитивно, то обратная проекция через произвольную функцию f сохраняет транспозицию.

LaTeX

$$$\forall {\beta} {r} {f},\ \mathrm{Transitive}(r) \rightarrow \mathrm{Transitive}(\mathrm{InvImage}(r,f))$$$

Lean4

theorem trans (h : Transitive r) : Transitive (InvImage r f) :=
  fun (a₁ a₂ a₃ : α) (h₁ : InvImage r f a₁ a₂) (h₂ : InvImage r f a₂ a₃) ↦ h h₁ h₂

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