scottContinuous — Mathlib

English

Same as above: if f is directed and f(i) ≤ a for all i, then ⨆ i, f(i) ≤ a.

Русский

То же, что выше: если f направлено и f(i) ≤ a для всех i, тогда ⨆ i f(i) ≤ a.

LaTeX

$$$\text{Directed}(\le)\ f \rightarrow (\forall i,\ f(i) \le a) \rightarrow \bigvee_{i} f(i) \le a$$$

Lean4

/-- Scott-continuity takes on a simpler form in complete partial orders. -/
theorem scottContinuous {f : α → β} :
    ScottContinuous f ↔ ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (· ≤ ·) d → IsLUB (f '' d) (f (sSup d)) :=
  by
  refine ⟨fun h d hd₁ hd₂ ↦ h hd₁ hd₂ hd₂.isLUB_sSup, fun h d hne hd a hda ↦ ?_⟩
  rw [hda.unique hd.isLUB_sSup]
  exact h hne hd

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