mono — Mathlib

English

If D contains all two-point directed sets {a,b} whenever a ≤ b, and f is Scott-continuous on D, then f is monotone.

Русский

Если в D для любых a ≤ b множество {a,b} принадлежит D, и f является Scott–непрерывной на D, то f монотонна.

LaTeX

$$$\\big(\\forall a,b,\\ a \\le b \\Rightarrow \\{a,b\\} \\in D\\big) \\to \\mathrm{ScottContinuousOn}(D,f) \\to \\text{Monotone}(f).$$$

Lean4

theorem mono (hD : D₁ ⊆ D₂) (hf : ScottContinuousOn D₂ f) : ScottContinuousOn D₁ f := fun _ hdD₁ hd₁ hd₂ _ hda =>
  hf (hD hdD₁) hd₁ hd₂ hda

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