codRestrict — Mathlib

English

For f : PrincipalSeg r s, and a, Acc r a is equivalent to Acc s (f a).

Русский

Для f : PrincipalSeg r s выполняется эквивалентность Acc r a и Acc s (f a).

LaTeX

$$$\\mathrm{Acc}(r, a) \\iff \\mathrm{Acc}(s, f(a))$$$

Lean4

/-- Restrict the codomain of a principal segment embedding. -/
def codRestrict (p : Set β) (f : r ≺i s) (H : ∀ a, f a ∈ p) (H₂ : f.top ∈ p) : r ≺i Subrel s (· ∈ p) :=
  ⟨RelEmbedding.codRestrict p f H, ⟨f.top, H₂⟩, fun ⟨_, _⟩ => by simp [← f.mem_range_iff_rel]⟩

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