Theorems · Theorem · general topology

Filter.HasBasis.mem_lift_iff

∀ {α : Type u_1} {γ : Type u_3} {ι : Sort u_6} {p : ι → Prop} {s : ι → Set α} {f : Filter α},
  f.HasBasis p s →
    ∀ {β : ι → Type u_5} {pg : (i : ι) → β i → Prop} {sg : (i : ι) → β i → Set γ} {g : Set α → Filter γ},
      (∀ (i : ι), (g (s i)).HasBasis (pg i) (sg i)) →
        Monotone g → ∀ {s : Set γ}, s ∈ f.lift g ↔ ∃ i, p i ∧ ∃ x, pg i x ∧ sg i x ⊆ s

If (p : ι → Prop, s : ι → Set α) is a basis of a filter f, g is a monotone function Set α → Filter γ, and for each i, (pg : β i → Prop, sg : β i → Set α) is a basis of the filter g (s i), then (fun (i : ι) (x : β i) ↦ p i ∧ pg i x, fun (i : ι) (x : β i) ↦ sg i x) is a basis of the filter f.lift g. This basis is parametrized by i : ι and x : β i, so in order to formulate this fact using Filter.HasBasis one has to use Σ i, β i as the index type, see Filter.HasBasis.lift. This lemma states the corresponding mem_iff statement without using a sigma type.

Defined in

Mathlib.Order.Filter.Lift

Cited by

3 results in Mathlib

Foundations

Depth 60 from the axioms · uses propext, Classical.choice, Quot.sound