LeanPool.AFormalizationOfBorelDeterminacyInLean.Applications.General

Auxiliary declarations for the Borel determinacy formalization.

theorem diff_subset_union {I : Type u_1} {A B C : Set I} : A \ C ⊆ A \ B ∪ B \ C

theorem projection_formula {α : Type u_1} {β : Type u_2} (f : α → β) (X : Set α) (Y : Set β) : Disjoint X (f ⁻¹' Y) ↔ Disjoint (f '' X) Y

theorem Filter.mem_congr {α : Type u_1} {s t : Set α} {l : Filter α} (h : s =ᶠ[l] t) : s ∈ l ↔ t ∈ l

theorem Filter.eventuallyEq_set' {α : Type u_4} {s t : Set α} {l : Filter α} : s =ᶠ[l] t ↔ (s \ t)ᶜ ∈ l ∧ (t \ s)ᶜ ∈ l