inf₂

Mathlib.Order.ScottContinuity.Complete

URI: https://scilib.ai/kg/mathlib#ScottContinuous.inf₂

← MathLib Explorer

English

The map (a,b) ↦ a ∧ b is Scott-continuous.

Русский

Отображение (a,b) ↦ a ∧ b является Scott–непрерывным.

LaTeX

$$$\\mathrm{ScottContinuous}\\big((a,b) \\mapsto a \\wedge b\\big).$$$

Lean4

theorem inf₂ : ScottContinuous fun (a, b) => (a ⊓ b : β) :=
  ScottContinuous.fromProd (fun a => scottContinuous_inf_right a) scottContinuous_inf_left

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru