preimage — Mathlib

English

Given an equivalence f: α ≃ β and a relation s on β, there is a natural RelIso between the preimage relation on α and s.

Русский

Дано эквивалентность f: α ≃ β и отношение s на β; существует естественный RelIso между отношением на префикс и s.

LaTeX

$$$$ \text{RelIso.preimage}(f,s) : (f^{-1})^*\,o\, s \cong_r s. $$$$

Lean4

/-- Any equivalence lifts to a relation isomorphism between `s` and its preimage. -/
protected def preimage (f : α ≃ β) (s : β → β → Prop) : f ⁻¹'o s ≃r s :=
  ⟨f, Iff.rfl⟩
    -- `simps` crashes if asked to generate these

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