monotone — Mathlib

English

If D1 ⊆ D2 then ScottContinuousOn D2 f implies ScottContinuousOn D1 f.

Русский

Если D1 ⊆ D2, то ScottContinuousOn D2 f влечёт ScottContinuousOn D1 f.

LaTeX

$$$D_1 \\subseteq D_2 \\to \\mathrm{ScottContinuousOn}(D_2,f) \\to \\mathrm{ScottContinuousOn}(D_1,f).$$$

Lean4

protected theorem monotone (D : Set (Set α)) (hD : ∀ a b : α, a ≤ b → { a, b } ∈ D) (h : ScottContinuousOn D f) :
    Monotone f :=
  by
  refine fun a b hab =>
    (h (hD a b hab) (insert_nonempty _ _) (directedOn_pair le_refl hab) ?_).1 (mem_image_of_mem _ <| mem_insert _ _)
  rw [IsLUB, upperBounds_insert, upperBounds_singleton, inter_eq_self_of_subset_right (Ici_subset_Ici.2 hab)]
  exact isLeast_Ici

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