scottContinuous_inf_left — Mathlib

English

Let β be a complete linear order. For every b ∈ β, the map a ↦ a ∧ b is Scott-continuous.

Русский

Пусть β — полная линейно упорядоченная совокупность. Для каждого b ∈ β отображение a ↦ a ∧ b является Scott–непрерывной.

LaTeX

$$$\\forall b \\in \\beta\\,\\mathrm{ScottContinuous}(a \\mapsto a \\wedge b).$$$

Lean4

theorem scottContinuous_inf_left (b : β) : ScottContinuous fun a ↦ a ⊓ b :=
  .of_map_sSup
    (fun d _ _ ↦ by rw [sSup_inf_eq, sSup_image])
      /- The meet operation is Scott continuous -/

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