preimage_prodMap — Mathlib

English

If t is transitive on Y and f: X → Y, then the pullback relation { (x1,x2) | (f x1, f x2) ∈ t } on X is transitive.

Русский

Если t транзитивно на Y и f: X → Y, то тяготеющее назад отношение на X по f также транзитивно.

LaTeX

$$$\text{Transitive}(t) \Rightarrow \text{Transitive}\big(\text{Preimage}(\mathrm{Prod.map}\ f\ f, t)\big)$$$

Lean4

theorem preimage_prodMap {Y : Type*} {t : Set (Y × Y)} (ht : IsTransitiveRel t) (f : X → Y) :
    IsTransitiveRel (Prod.map f f ⁻¹' t) := fun _ _ _ h h' ↦ ht h h'

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