prod_subset_trans — Mathlib

English

If s is transitive, and t×ˢu ⊆ s, u×ˢv ⊆ s, and u is nonempty, then t×ˢv ⊆ s.

Русский

Если s транзитивно, t×ˢu ⊆ s, u×ˢv ⊆ s и u непусто, то t×ˢv ⊆ s.

LaTeX

$$$\text{Transitive}(s) \rightarrow (t \timesˢ u \subseteq s) \rightarrow (u \timesˢ v \subseteq s) \rightarrow u \neq \emptyset \rightarrow (t \timesˢ v \subseteq s)$$$

Lean4

theorem prod_subset_trans {s : Set (X × X)} {t u v : Set X} (hs : IsTransitiveRel s) (htu : t ×ˢ u ⊆ s)
    (huv : u ×ˢ v ⊆ s) (hu : u.Nonempty) : t ×ˢ v ⊆ s :=
  by
  rintro ⟨a, b⟩ hab
  simp only [mem_prod] at hab
  obtain ⟨x, hx⟩ := hu
  exact hs (@htu ⟨a, x⟩ ⟨hab.left, hx⟩) (@huv ⟨x, b⟩ ⟨hx, hab.right⟩)

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