cbiInf_eq_of_not_forall — Mathlib

English

In a ConditionallyCompleteLinearOrder, if not all i satisfy p(i), then the global infimum over i with p(i) equals the infimum over all i of f, intersected with the infimum of the empty set.

Русский

В частично полностью линейном порядке, если не все i удовлетворяют p(i), тогда общий infimum по i с p(i) равен infimum по всем i пересечение infimum пустого набора.

LaTeX

$$$\neg (\forall i, p(i)) \Rightarrow iInf (i) (h : p(i)) \; f\langle i, h\rangle = iInf f \; \wedge\; sInf \emptyset$$$

Lean4

theorem cbiInf_eq_of_not_forall {p : ι → Prop} {f : Subtype p → α} (hp : ¬(∀ i, p i)) :
    ⨅ (i) (h : p i), f ⟨i, h⟩ = iInf f ⊓ sInf ∅ :=
  cbiSup_eq_of_not_forall (α := αᵒᵈ) hp

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