eq_preimage — Mathlib

English

Let f be a RelEmbedding from (α, r) to (β, s). Then r is exactly the pullback of s along f; equivalently, for all a,b ∈ α, r(a,b) holds if and only if s(f(a), f(b)).

Русский

Пусть f — вложение отношений from (α, r) к (β, s). Тогда r является точным предобразом (pullback) s вдоль f; то есть для любых a,b ∈ α выполняется r(a,b) тогда и только тогда, когда s(f(a), f(b)).

LaTeX

$$$\forall a,b.\ r(a,b) \iff s\bigl(f(a), f(b)\bigr)$$$

Lean4

theorem eq_preimage (f : r ↪r s) : r = f ⁻¹'o s := by
  ext a b
  exact f.map_rel_iff.symm

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