compRel — Mathlib

English

If S and T are nonempty and S ×ˢ T ⊆ idRel, then there exists x with S = {x} and T = {x}.

Русский

Если S и T непустые и S ×ˢ T ⊆ idRel, то существует x такое, что S = {x} и T = {x}.

LaTeX

$$$S\\neq \\varnothing \\land T\\neq \\varnothing \\land S\\timesˢ T \\subseteq idRel \\Rightarrow \\exists x, S={x} \\land T={x}$$$

Lean4

/-- The composition of relations -/
def compRel (r₁ r₂ : Set (α × α)) :=
  {p : α × α | ∃ z : α, (p.1, z) ∈ r₁ ∧ (z, p.2) ∈ r₂}

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