English
Variant with HasBasis, giving an explicit witness function with membership properties preserved.
Русский
Вариант с HasBasis, дающий явный свидетелЬ функции, сохраняющей принадлежности.
LaTeX
$$Exists f : ι → β, ∀ i, x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b i$$
Lean4
/-- Writing a liminf as a supremum of infimum, in a (possibly non-complete) conditionally complete
linear order. A reparametrization trick is needed to avoid taking the infimum of sets which are
not bounded below. -/
theorem liminf_eq_ite {v : Filter ι} {p : ι' → Prop} {s : ι' → Set ι} [Countable (Subtype p)] [Nonempty (Subtype p)]
(hv : v.HasBasis p s) (f : ι → α) :
liminf f v =
if ∃ (j : Subtype p), s j = ∅ then sSup univ
else
if ∀ (j : Subtype p), ¬BddBelow (range (fun (i : s j) ↦ f i)) then sSup ∅
else ⨆ (j : Subtype p), ⨅ (i : s (liminf_reparam f s p j)), f i :=
by
by_cases H : ∃ (j : Subtype p), s j = ∅
· rw [if_pos H]
rcases H with ⟨j, hj⟩
simp [hv.liminf_eq_sSup_univ_of_empty j j.2 hj]
rw [if_neg H]
by_cases H' : ∀ (j : Subtype p), ¬BddBelow (range (fun (i : s j) ↦ f i))
· have A : ∀ (j : Subtype p), ⋂ (i : s j), Iic (f i) = ∅ :=
by
simp_rw [← not_nonempty_iff_eq_empty, nonempty_iInter_Iic_iff]
exact H'
simp_rw [if_pos H', hv.liminf_eq_sSup_iUnion_iInter, A, iUnion_empty]
rw [if_neg H']
apply hv.liminf_eq_ciSup_ciInf
· push_neg at H
simpa only [nonempty_iff_ne_empty] using H
· push_neg at H'
exact H'
