English
If β is finite, then any L with LeAtTop and NeBot equals the unconditional β.
Русский
Если β конечно, то любой L с LeAtTop и NeBot равен безусловному фильтру β.
LaTeX
$$$[\\text{Finite }\\beta]\\;\\Rightarrow\\; (L=[[\\text{unconditional }\\beta]])$$$
Lean4
/-- If `β` is finite, then `unconditional β` is the only summation filter `L` on `β` satisfying
`L.LeAtTop` and `L.NeBot`. -/
theorem eq_unconditional_of_finite {β} [Finite β] (L : SummationFilter β) [L.LeAtTop] [L.NeBot] : L = unconditional β :=
by
classical
haveI := Fintype.ofFinite β
have hAtTop : (atTop : Filter (Finset β)) = pure Finset.univ := by
rw [(isTop_iff_eq_top.mpr rfl).atTop_eq (a := Finset.univ), ← Finset.top_eq_univ, Ici_top, principal_singleton]
have hL := L.le_atTop
have hL' : ∅ ∉ L.filter := empty_mem_iff_bot.not.mpr <| NeBot.ne_bot.ne'
cases L with
| mk F =>
simp only [unconditional, hAtTop] at *
congr 1
refine eq_of_le_of_ge hL (pure_le_iff.mpr ?_)
contrapose! hL'
obtain ⟨s, hs, hs'⟩ := hL'
simpa [inter_singleton_eq_empty.mpr hs'] using inter_mem hs (le_pure_iff.mp hL)
