codRestrict — Mathlib

English

Restrict the codomain of a relation embedding along a predicate p on β, obtaining a new embedding into Subrel s (· ∈ p).

Русский

Ограничение кодом отображения отношения вдоль предиката p на β, получающее новое вложение в Subrel s (· ∈ p).

LaTeX

$$$ codRestrict\\; (p : Set\\; \\beta)\\ (f : r \\hookrightarrow r\\; s)\\ (H : ∀ a, f\\ a ∈ p) : r \\hookrightarrow r\\; Subrel\\; s (\\;\\cdot ∈ p\\;) $$$

Lean4

/-- Restrict the codomain of a relation embedding. -/
def codRestrict (p : Set β) (f : r ↪r s) (H : ∀ a, f a ∈ p) : r ↪r Subrel s (· ∈ p) :=
  ⟨f.toEmbedding.codRestrict p H, f.map_rel_iff'⟩

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