codirectedOn — Mathlib

English

If s is inf-closed and a is in upperBounds s, then insert a into s is inf-closed.

Русский

Если s инф-замкнуто и a ∈ upperBounds s, то вставка a в s сохраняет инф-замкнутость.

LaTeX

$$$ (\\text{InfClosed } s) \\rightarrow (a \\in \\text{upperBounds } s) \\rightarrow \\text{InfClosed}(\\operatorname{insert} a s) $$$

Lean4

theorem codirectedOn (hs : InfClosed s) : DirectedOn (· ≥ ·) s := fun _a ha _b hb ↦
  ⟨_, hs ha hb, inf_le_left, inf_le_right⟩

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