valuation_isClosedMap — Mathlib

English

The valuation map is a closed map: its image of a closed set is closed.

Русский

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

LaTeX

$$$IsClosedMap(v: K \to Γ_0)$$$

Lean4

theorem valuation_isClosedMap : IsClosedMap (v : K → Γ₀) :=
  by
  refine IsClosedMap.of_nonempty ?_
  intro U hU hU'
  simp only [← isOpen_compl_iff, isOpen_iff_mem_nhds, mem_compl_iff, mem_nhds, subset_compl_comm, compl_setOf,
    not_lt] at hU
  simp only [isClosed_iff, mem_image, map_eq_zero, exists_eq_right, ne_eq, image_subset_iff]
  refine (em _).imp_right fun h ↦ ?_
  obtain ⟨γ, h⟩ := hU _ h
  simp only [sub_zero] at h
  refine ⟨γ, γ.ne_zero, h.trans ?_⟩
  intro
  simp

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