isBoundedUnder_ge_inf — Mathlib

English

For a semilatticeInf α, the statement IsBoundedUnder (≥) for a function a ↦ u(a) ⊓ v(a) is equivalent to both IsBoundedUnder (≥) for u and for v separately.

Русский

Для полусортированного множества сInf эквивалентно: IsBoundedUnder (≥) для u и для v вместе эквивалентно IsBoundedUnder (≥) для их_infimum.

LaTeX

$$$\operatorname{IsBoundedUnder}(\ge, l)(u\inf v) \iff \left(\operatorname{IsBoundedUnder}(\ge, l)u \land \operatorname{IsBoundedUnder}(\ge, l)v\right)$$$

Lean4

@[simp]
theorem isBoundedUnder_ge_inf [SemilatticeInf α] {f : Filter β} {u v : β → α} :
    (f.IsBoundedUnder (· ≥ ·) fun a => u a ⊓ v a) ↔ f.IsBoundedUnder (· ≥ ·) u ∧ f.IsBoundedUnder (· ≥ ·) v :=
  isBoundedUnder_le_sup (α := αᵒᵈ)

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