Filter.Basic

コード元 Filter.Basic

このファイルではフィルタの基本的な性質を定義しています.

theorem Eventually.of_forall {p : α → Prop} {f : Filter α} (hp : ∀ x, p x) : ∀ᶠ x in f, p x :=
  univ_mem' hp

Eventually.of_forallは全てのxについてpが成り立てば, “十分大きな”xについてpが成り立つことを述べた主張です.ここでmem_of_supersetとuniv_mem'は以下の定理になります.

theorem mem_of_superset {x y : Set α} (hx : x ∈ f) (hxy : x ⊆ y) : y ∈ f :=
  f.sets_of_superset hx hxy

theorem univ_mem' (h : ∀ a, a ∈ s) : s ∈ f :=
  mem_of_superset univ_mem fun x _ => h x

ちなみにuniv_mem'のfun x _ => h xは∀ x ∈ Set.univ, x ∈ sですが, Set.Subsetの定義よりこれはSet.univ ⊆ sそのものです.