mem_compRel — Mathlib

English

For r1, r2 subsets of α×α, (x,y) ∈ r1 ○ r2 iff there exists z with (x,z) ∈ r1 and (z,y) ∈ r2.

Русский

Для подмножеств r1, r2 ⊆ α×α, (x,y) ∈ r1 ○ r2 тогда и только тогда, когда существует z, такое что (x,z) ∈ r1 и (z,y) ∈ r2.

LaTeX

$$$\\forall {α} {r1 r2 : Set (α \\times α)} {x y : α}, (x,y) \\in r1 \\circ r2 \\iff \\exists z, (x,z) \\in r1 \\land (z,y) \\in r2$$$

Lean4

@[simp]
theorem mem_compRel {α : Type u} {r₁ r₂ : Set (α × α)} {x y : α} : (x, y) ∈ r₁ ○ r₂ ↔ ∃ z, (x, z) ∈ r₁ ∧ (z, y) ∈ r₂ :=
  Iff.rfl

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