codRestrict — Mathlib

English

Restrict the codomain of an initial segment to a subset p of β, via a witness H that f a ∈ p for all a.

Русский

Ограничить кодовую часть начального отрезка до подмножества p ⊆ β с помощью свидетельства H, что f a ∈ p для всех a.

LaTeX

$$$codRestrict(p)(f) : r \\preccurlyeq_i Subrel(s, \\lambda x. x \\in p).$$$

Lean4

/-- Restrict the codomain of an initial segment -/
def codRestrict (p : Set β) (f : r ≼i s) (H : ∀ a, f a ∈ p) : r ≼i Subrel s (· ∈ p) :=
  ⟨RelEmbedding.codRestrict p f H, fun a ⟨b, m⟩ h =>
    let ⟨a', e⟩ := f.mem_range_of_rel h
    ⟨a', by subst e; rfl⟩⟩

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