Map — Mathlib

English

If f is the identity, then r ∘r (·=·) = r.

Русский

Если f является тождественным отображением, то r ∘r (=) = r.

LaTeX

$$$\forall r:\alpha\to\beta\to \mathrm{Prop},\; r \circ_r (\cdot=\cdot) = r$$$

Lean4

/-- The map of a relation `r` through a pair of functions pushes the
relation to the codomains of the functions.  The resulting relation is
defined by having pairs of terms related if they have preimages
related by `r`.
-/
protected def Map (r : α → β → Prop) (f : α → γ) (g : β → δ) : γ → δ → Prop := fun c d ↦
  ∃ a b, r a b ∧ f a = c ∧ g b = d

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