codRestrict_restrict — Mathlib

English

Restriction commutes with the projection to the domain, i.e., restricting and then projecting equals projecting and then restricting.

Русский

Ограничение и проекция совместимы: ограничение затем проекция равно проекции затем ограничение.

LaTeX

$$$\\operatorname{coe}\\circ h.restrict = s.restrict f$$$

Lean4

/-- Restricting the domain and then the codomain is the same as `MapsTo.restrict`. -/
@[simp]
theorem codRestrict_restrict (h : ∀ x : s, f x ∈ t) :
    codRestrict (s.restrict f) t h = MapsTo.restrict f s t fun x hx => h ⟨x, hx⟩ :=
  rfl

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