comp — Mathlib

English

A binary product of proper maps is proper.

Русский

Двоичное произведение правильных отображений проперно.

LaTeX

$$$\mathrm{IsProperMap}(f) \land \mathrm{IsProperMap}(g) \Rightarrow \mathrm{IsProperMap}(\mathrm{Prod.map} \, f \, g)$$$

Lean4

/-- The composition of two proper maps is proper. -/
theorem comp (hg : IsProperMap g) (hf : IsProperMap f) : IsProperMap (g ∘ f) :=
  by
  refine ⟨by fun_prop, fun ℱ z h ↦ ?_⟩
  rw [mapClusterPt_comp] at h
  rcases hg.clusterPt_of_mapClusterPt h with ⟨y, rfl, hy⟩
  rcases hf.clusterPt_of_mapClusterPt hy with ⟨x, rfl, hx⟩
  use x, rfl

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