continuous_inf — Mathlib

English

The infimum map (x,y) ↦ x ⊓ y is continuous in a topological lattice when inf is continuous.

Русский

КартаInf (х,у) ↦ x ⊓ y непрерывна в топологической решетке, если инфимум непрерывен.

LaTeX

$$$\\text{Continuous}(\\lambda p:\\,L\\times L, p_1 \\wedge p_2)$$$

Lean4

@[continuity]
theorem continuous_inf [Min L] [ContinuousInf L] : Continuous fun p : L × L => p.1 ⊓ p.2 :=
  ContinuousInf.continuous_inf

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