exists_eq_ciInf_of_not_isPredPrelimit

English

Let α be a conditionally complete linear order and f: ι → α with range f bounded below. If ⨅ i, f(i) is not a pred-prelimit, then there exists i with f(i) = ⨅ i, f(i).

Русский

Пусть α — линейный порядок с условной полнотой и f: ι → α так, чтобы множество значений f было ограничено снизу. Если нижний предел верх, определяемый как inf_i f(i), не является пред-предельным пределом, существует индекс i, для которого f(i) достигает этого инфима.

LaTeX

$$$ BddBelow(\\mathrm{range}(f)) \\land \\neg IsPredPrelimit (\\inf_i f(i)) \\Rightarrow \\exists i\, f(i) = \\inf_i f(i) $$$

Lean4

theorem exists_eq_ciInf_of_not_isPredPrelimit (hf : BddBelow (range f)) (hf' : ¬IsPredPrelimit (⨅ i, f i)) :
    ∃ i, f i = ⨅ i, f i :=
  csInf_mem_of_not_isPredPrelimit (range_nonempty f) hf hf'

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