generalizingMap — Mathlib

English

If f is inducing and its range is stable under generalization, then f is generalizing.

Русский

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

LaTeX

$$$\\\\text{IsInducing}(f) \\\\land \\\\mathrm{StableUnderGeneralization}(\\\\mathrm{range}(f)) \\\\Rightarrow \\\\text{GeneralizingMap}(f).$$$

Lean4

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

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