embDomain_mapRange — Mathlib

English

There is a linear order instance on DegLex(Finsupp α Nat) provided the underlying LT on α.

Русский

Существует экземпляр линейного порядка на DegLex(Finsupp α Nat), если задан линейный порядок на α.

LaTeX

$$LT (DegLex (Finsupp α Nat))$$

Lean4

theorem embDomain_mapRange (f : α ↪ β) (g : M → N) (p : α →₀ M) (hg : g 0 = 0) :
    embDomain f (mapRange g hg p) = mapRange g hg (embDomain f p) :=
  by
  ext a
  by_cases h : a ∈ Set.range f
  · rcases h with ⟨a', rfl⟩
    rw [mapRange_apply, embDomain_apply, embDomain_apply, mapRange_apply]
  · rw [mapRange_apply, embDomain_notin_range, embDomain_notin_range, ← hg] <;> assumption

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