specializingMap — Mathlib

English

If f is an inducing map and the range of f is stable under specialization, then f is specializing.

Русский

Если f — индуктивное отображение и образ диапазона f стабилен по специализации, то f является специализирующим отображением.

LaTeX

$$$\\\\text{IsInducing}(f) \\\\land \\\\mathrm{StableUnderSpecialization}(\\\\mathrm{range}(f)) \\\\Rightarrow \\\\text{SpecializingMap}(f).$$$

Lean4

theorem specializingMap (hf : IsInducing f) (h : StableUnderSpecialization (range f)) : SpecializingMap f :=
  by
  intro x y e
  obtain ⟨y, rfl⟩ := h e ⟨x, rfl⟩
  exact ⟨_, hf.specializes_iff.mp e, rfl⟩

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