entourageProd — Mathlib

English

If s ⊆ X×X and t ⊆ Y×Y are transitive relations, then their entourage product entorageProd(s,t) is transitive.

Русский

Если s ⊆ X×X и t ⊆ Y×Y — транзитивные отношения, то их произведение окружений entourageProd(s,t) транзитивно.

LaTeX

$$$IsTransitiveRel\big( entou rageProd(s,t) \big)$$$

Lean4

theorem entourageProd {s : Set (X × X)} {t : Set (Y × Y)} (hs : IsTransitiveRel s) (ht : IsTransitiveRel t) :
    IsTransitiveRel (entourageProd s t) := fun _ _ _ h h' ↦ ⟨hs h.left h'.left, ht h.right h'.right⟩

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