English
The exterior σ-algebras of finite coordinate sets form a cofiltration indexed by Finset α, i.e., they decrease with increasing coordinate complement size.
Русский
Внешние сигма-алгебры конечных координат образуют кофильтрацию, индексируемую Finset α; они убывают при увеличении множества координат вне Λ.
LaTeX
$$$\text{The family }\{\mathcal{F}_\Lambda\}_{\Lambda\subseteq_f \alpha} \text{ is a cofiltration with } \mathcal{F}_{\Lambda_1} \supseteq \mathcal{F}_{\Lambda_2}\text{ if } \Lambda_1 \subseteq \Lambda_2.$$$
Lean4
theorem hitting_mem_set [WellFoundedLT ι] {m : ι} (h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s) :
u (hitting u s n m ω) ω ∈ s := by
simp_rw [hitting, if_pos h_exists]
have h_nonempty : (Set.Icc n m ∩ {i : ι | u i ω ∈ s}).Nonempty :=
by
obtain ⟨k, hk₁, hk₂⟩ := h_exists
exact ⟨k, Set.mem_inter hk₁ hk₂⟩
have h_mem := csInf_mem h_nonempty
rw [Set.mem_inter_iff] at h_mem
exact h_mem.2
