rel_comp_apply₂ — Mathlib

English

For a RelCat X — Y — Z and arrows f: X ⟶ Y, g: Y ⟶ Z, two elements x ∈ X, z ∈ Z are related by (f ≫ g).rel iff there exists y ∈ Y with x related by f.rel to y and y related by g.rel to z.

Русский

Для RelCat X — Y — Z и стрел f: X ⟶ Y, g: Y ⟶ Z: x ∈ X и z ∈ Z связаны через (f ≫ g).rel тогда и только тогда, когда найдётся y ∈ Y, такой что x связан с y rel через f.rel и y связан с z rel через g.rel.

LaTeX

$$theorem rel_comp_apply₂ (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) (z : Z) :\n x ~[(f ≫ g).rel] z ↔ ∃ y, x ~[f.rel] y ∧ y ~[g.rel] z :=\n .rfl$$

Lean4

theorem rel_comp_apply₂ (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) (z : Z) :
    x ~[(f ≫ g).rel] z ↔ ∃ y, x ~[f.rel] y ∧ y ~[g.rel] z :=
  .rfl

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