scottContinuous_inf_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem scottContinuous_inf_right (a : β) : ScottContinuous fun b ↦ a ⊓ b :=
  .of_map_sSup (fun d _ _ ↦ by rw [inf_sSup_eq, sSup_image])

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