LeanPool.AFormalizationOfBorelDeterminacyInLean.Applications.Meager

Auxiliary declarations for the Borel determinacy formalization.

def Topology.DenseOf : Lean.ParserDescr

Auxiliary declaration for the Borel determinacy formalization.

Equations

• One or more equations did not get rendered due to their size.

theorem dense_trans {X : Type u_1} [tX : TopologicalSpace X] {A : Set X} {B : Set ↑A} (hA : Dense A) (hB : Dense B) : Dense (Subtype.val '' B)

theorem dense_in_closure {X : Type u_1} [tX : TopologicalSpace X] (A : Set X) : Dense (Subtype.val ⁻¹' A)

def openDenseFilterBasis {X : Type u_1} [tX : TopologicalSpace X] : FilterBasis X

Auxiliary declaration for the Borel determinacy formalization.

Equations

• openDenseFilterBasis = { sets := {U : Set X | IsOpen U ∧ Dense U}, nonempty := ⋯, inter_sets := ⋯ }

@[reducible, inline]

abbrev openDenseFilter {X : Type u_1} [tX : TopologicalSpace X] : Filter X

Auxiliary declaration for the Borel determinacy formalization.

Equations

• openDenseFilter = openDenseFilterBasis.filter

theorem IsNowhereDense.inter_left {X : Type u_1} [tX : TopologicalSpace X] {A B : Set X} (hA : IsNowhereDense A) : IsNowhereDense (A ∩ B)

theorem IsNowhereDense.inter_right {X : Type u_1} [tX : TopologicalSpace X] {A B : Set X} (hA : IsNowhereDense A) : IsNowhereDense (B ∩ A)

theorem isNowhereDense_iff_subset_closed_nowhereDense {X : Type u_1} [tX : TopologicalSpace X] {A : Set X} : IsNowhereDense A ↔ ∃ (C : Set X), A ⊆ C ∧ IsClosed C ∧ IsNowhereDense C

theorem isNowhereDense_iff_compl_contains_openDense {X : Type u_1} [tX : TopologicalSpace X] {A : Set X} : IsNowhereDense A ↔ Aᶜ ∈ openDenseFilter

theorem isNowhereDense.union {X : Type u_1} [tX : TopologicalSpace X] {A B : Set X} (hA : IsNowhereDense A) (hB : IsNowhereDense B) : IsNowhereDense (A ∪ B)

theorem isNowhereDense_iUnion {X : Type u_1} [tX : TopologicalSpace X] {I : Sort u_3} {A : I → Set X} [Finite I] (h : ∀ (i : I), IsNowhereDense (A i)) : IsNowhereDense (⋃ (i : I), A i)

theorem tendsto_openDense_of_isOpenMap {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (f : X → Y) (hc : Continuous f) (ho : IsOpenMap f) : Filter.Tendsto f openDenseFilter openDenseFilter

theorem IsNowhereDense.preimage {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (f : X → Y) {A : Set Y} (h : IsNowhereDense A) (hc : Continuous f) (ho : IsOpenMap f) : IsNowhereDense (f ⁻¹' A)

theorem Dense.dense_in_open {X : Type u_1} [tX : TopologicalSpace X] {A U : Set X} (hU : IsOpen U) (hD : Dense A) : Dense (Subtype.val ⁻¹' A)

theorem somewhereDense_iff {X : Type u_1} [tX : TopologicalSpace X] {A : Set X} : ¬IsNowhereDense A ↔ ∃ (U : Set X), U.Nonempty ∧ IsOpen U ∧ Dense (Subtype.val ⁻¹' A)

theorem nowhereDense_iff {X : Type u_1} [tX : TopologicalSpace X] {A : Set X} : IsNowhereDense A ↔ ∀ (U : Set X), U.Nonempty → IsOpen U → ¬Dense (Subtype.val ⁻¹' A)

theorem isNowhereDense_image {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (f : X → Y) {A : Set X} (hf : Topology.IsInducing f) (h : IsNowhereDense A) : IsNowhereDense (f '' A)

theorem nowhereDense_in_open {X : Type u_1} [tX : TopologicalSpace X] {U : Set X} (hU : IsOpen U) (A : Set ↑U) : IsNowhereDense (Subtype.val '' A) ↔ IsNowhereDense A

theorem nowhereDense_in_dense {X : Type u_1} [tX : TopologicalSpace X] {U : Set X} (hU : Dense U) (A : Set ↑U) : IsNowhereDense (Subtype.val '' A) ↔ IsNowhereDense A

theorem isOpen_isNowhereDense {X : Type u_1} [tX : TopologicalSpace X] {U : Set X} (hU : IsOpen U) : IsNowhereDense U ↔ U = ∅

theorem Dense.somewhereDense {X : Type u_1} [tX : TopologicalSpace X] {U : Set X} [Nonempty X] (hU : Dense U) : ¬IsNowhereDense U

theorem nonempty_of_somewhereDense {X : Type u_1} [tX : TopologicalSpace X] {A : Set X} (h : ¬IsNowhereDense A) : Nonempty ↑A

theorem fiber_somewhereDense {X : Type u_1} [tX : TopologicalSpace X] {U : Set X} (h : ¬IsNowhereDense U) {α : Type u_3} (f : ↑U → α) [Finite α] : ∃ (a : α), ¬IsNowhereDense (Subtype.val '' f ⁻¹' {a})

theorem closure_open_cover {X : Type u_1} [tX : TopologicalSpace X] {A : Set X} {I : Sort u_3} (U : I → Set X) (hO : ∀ (i : I), IsOpen (U i)) (hcov : ⋃ (i : I), U i = Set.univ) : closure A = ⋃ (i : I), closure (A ∩ U i)

theorem interior_open_cover {X : Type u_1} [tX : TopologicalSpace X] {A : Set X} {I : Sort u_3} (U : I → Set X) (hO : ∀ (i : I), IsOpen (U i)) (hcov : ⋃ (i : I), U i = Set.univ) : interior A = ⋃ (i : I), interior (A ∩ U i)

theorem open_cover_closed {X : Type u_1} [tX : TopologicalSpace X] {I : Type u_3} (U : I → Set X) (hO : ∀ (i : I), IsOpen (U i)) (hcov : ⋃ (i : I), U i = Set.univ) (hd : Pairwise (Function.onFun Disjoint U)) (i : I) : IsClosed (U i)

theorem IsClopen.inter_closure {X : Type u_1} [tX : TopologicalSpace X] {U : Set X} (h : IsClopen U) {A : Set X} : closure A ∩ U = closure (A ∩ U)

theorem nowhereDense_iff_nowhereDense_in_open {X : Type u_1} [tX : TopologicalSpace X] {A U : Set X} (hU : IsOpen U) (hA : A ⊆ U) : IsNowhereDense A ↔ IsNowhereDense (Subtype.val ⁻¹' A)

theorem isNowhereDense_disjoint_open {X : Type u_1} [tX : TopologicalSpace X] {A : Set X} {I : Type u_3} (U : I → Set X) (hO : ∀ (i : I), IsOpen (U i)) (hcov : A ⊆ ⋃ (i : I), U i) (hd : Pairwise (Function.onFun Disjoint U)) (h : ∀ (i : I), IsNowhereDense (A ∩ U i)) : IsNowhereDense A

theorem residual_le_openDense {X : Type u_1} [tX : TopologicalSpace X] : residual X ≤ openDenseFilter

theorem isMeagre_iff_eq_countable_union_isNowhereDense {X : Type u_1} [tX : TopologicalSpace X] {s : Set X} : IsMeagre s ↔ ∃ (S : Set (Set X)), (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s = ⋃₀ S

theorem IsMeagre.eq_countable_union_isNowhereDense {X : Type u_1} [tX : TopologicalSpace X] {A : Set X} (h : IsMeagre A) : ∃ (f : ℕ → ↑{t : Set X | IsNowhereDense t}), A = ⋃ (n : ℕ), ↑(f n)

theorem IsMeagre.interior {X : Type u_1} [tX : TopologicalSpace X] [BaireSpace X] {U : Set X} (hU : IsMeagre U) : _root_.interior U = ∅

theorem isMeagre_image {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (f : X → Y) {A : Set X} (hf : Topology.IsInducing f) (h : IsMeagre A) : IsMeagre (f '' A)

theorem isMeagre_congr {X : Type u_1} [tX : TopologicalSpace X] {A B : Set X} (h : A =ᶠ[residual X] B) : IsMeagre A ↔ IsMeagre B

theorem baireSpace_iff_isMeagre_interior {X : Type u_1} [tX : TopologicalSpace X] : BaireSpace X ↔ ∀ (U : Set X), IsMeagre U → interior U = ∅

theorem isOpen_isMeagre {X : Type u_1} [tX : TopologicalSpace X] [BaireSpace X] {U : Set X} (hU : IsOpen U) : IsMeagre U ↔ U = ∅

theorem baireSpace_iff_isMeagre_isOpen {X : Type u_1} [tX : TopologicalSpace X] : BaireSpace X ↔ ∀ (U : Set X), IsMeagre U → IsOpen U → U = ∅

theorem open_baire {X : Type u_1} [tX : TopologicalSpace X] [BaireSpace X] {U : Set X} (hU : IsOpen U) : BaireSpace ↑U

def residual.dom.Forces {X : Type u_1} [tX : TopologicalSpace X] (U : TopologicalSpace.Opens X) (A : Set X) : Prop

Auxiliary declaration for the Borel determinacy formalization.

Equations

• residual.dom.Forces U A = (Subtype.val ⁻¹' A ∈ residual ↑↑U)

def residual.dom.«term_⊩_» : Lean.TrailingParserDescr

Auxiliary declaration for the Borel determinacy formalization.

Equations

• residual.dom.«term_⊩_» = Lean.ParserDescr.trailingNode `residual.dom.«term_⊩_» 50 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊩ ") (Lean.ParserDescr.cat `term 50))

theorem residual.dom.forces_iff_isMeagre {X : Type u_1} [tX : TopologicalSpace X] {A : Set X} {U : TopologicalSpace.Opens X} : Forces U A ↔ IsMeagre (↑U \ A)

theorem residual.dom.forces_empty_iff_isMeagre {X : Type u_1} [tX : TopologicalSpace X] {U : TopologicalSpace.Opens X} : Forces U ∅ ↔ IsMeagre ↑U

theorem residual.dom.forces_mono_left {X : Type u_1} [tX : TopologicalSpace X] {A : Set X} {U V : TopologicalSpace.Opens X} (h : Forces V A) (hUV : U.carrier ⊆ V.carrier) : Forces U A

theorem residual.dom.forces_mono_right {X : Type u_1} [tX : TopologicalSpace X] {A B : Set X} {U : TopologicalSpace.Opens X} (h : Forces U A) (hAB : A ⊆ B) : Forces U B

theorem residual.dom.forces_iInter_right {X : Type u_1} [tX : TopologicalSpace X] {U : TopologicalSpace.Opens X} {I : Sort u_3} [Countable I] (A : I → Set X) (h : ∀ (i : I), Forces U (A i)) : Forces U (⋂ (i : I), A i)

theorem residual.dom.forces_rfl {X : Type u_1} [tX : TopologicalSpace X] {U : TopologicalSpace.Opens X} : Forces U ↑U

theorem residual.dom.forces_trans {X : Type u_1} [tX : TopologicalSpace X] {A : Set X} {U V : TopologicalSpace.Opens X} (hU : Forces U ↑V) (h : Forces V A) : Forces U A

theorem residual.dom.forces_congr {X : Type u_1} [tX : TopologicalSpace X] {A B : Set X} {U : TopologicalSpace.Opens X} (h : A =ᶠ[residual X] B) : Forces U A ↔ Forces U B

def dom {X : Type u_1} [tX : TopologicalSpace X] (A : Set X) : TopologicalSpace.Opens X

a Baire category analogue of outer measure

Equations

• dom A = ⨆ (U : TopologicalSpace.Opens X), ⨆ (_ : residual.dom.Forces U A), U

theorem residual.dom.congr {X : Type u_1} [tX : TopologicalSpace X] {A B : Set X} (h : A =ᶠ[residual X] B) : dom A = dom B

theorem residual.dom.forces {X : Type u_1} [tX : TopologicalSpace X] {A : Set X} : Forces (dom A) A

theorem residual.dom.forces_iff_le_dom {X : Type u_1} [tX : TopologicalSpace X] {A : Set X} {U : TopologicalSpace.Opens X} : Forces U A ↔ U ≤ dom A

theorem residual.dom.forces_iff_subset_dom {X : Type u_1} [tX : TopologicalSpace X] {A : Set X} {U : TopologicalSpace.Opens X} : Forces U A ↔ ↑U ⊆ ↑(dom A)

theorem residual.dom.forces_iUnion_left {X : Type u_1} [tX : TopologicalSpace X] {A : Set X} {I : Sort u_3} (U : I → TopologicalSpace.Opens X) (h : ∀ (i : I), Forces (U i) A) : Forces (⨆ (i : I), U i) A

theorem residual.dom.dom_empty_isMeagre {X : Type u_1} [tX : TopologicalSpace X] : IsMeagre ↑(dom ∅)

theorem residual.dom.banach_category {X : Type u_1} [tX : TopologicalSpace X] {I : Sort u_3} (U : I → Set X) (hUo : ∀ (i : I), IsOpen (U i)) (hUm : ∀ (i : I), IsMeagre (U i)) : IsMeagre (⋃ (i : I), U i)

theorem residual.dom.isRegular {X : Type u_1} [tX : TopologicalSpace X] {A : Set X} : Heyting.IsRegular (dom A)

theorem residual.dom.eq_residual {X : Type u_1} [tX : TopologicalSpace X] {A : Set X} (h : BaireMeasurableSet A) : A =ᶠ[residual X] ↑(dom A)