monotone_iff_continuous — Mathlib

English

Theorem is a restatement of isLowerSet_iff_nhds simplifying an equality of nhds

Русский

Теорема упрощает isLowerSet_iff_nhds для упрощенного равенства 𝓝дa

LaTeX

$$$$ \\text{isLowerSet}_\\text{simp}_1: \\text{IsLowerSet}(α) \\iff \\forall a, \\mathcal{N}(a) = \\mathcal{P}(\\mathrm{Iic}(a)). $$$$

Lean4

protected theorem monotone_iff_continuous [TopologicalSpace α] [TopologicalSpace β] [Topology.IsLowerSet α]
    [Topology.IsLowerSet β] {f : α → β} : Monotone f ↔ Continuous f :=
  by
  rw [← monotone_dual_iff]
  exact IsUpperSet.monotone_iff_continuous (α := αᵒᵈ) (β := βᵒᵈ) (f := (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ))

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