exists_iInter_of_mem_iInf — Mathlib

English

If s ∈ ⨅ i f i, then there exists V_i ∈ f i for all i, such that s = ⋂ i V_i.

Русский

Если s ∈ ⨅ i f i, то существует V_i ∈ f i для всех i, такой что s = ⋂ i V_i.

LaTeX

$$$ s \in \iInf_i f_i \Rightarrow \exists V: i \to Set α,\; (\forall i, V_i \in f_i) \land s = \bigcap_i V_i $$

Lean4

theorem exists_iInter_of_mem_iInf {ι : Sort*} {α : Type*} {f : ι → Filter α} {s} (hs : s ∈ ⨅ i, f i) :
    ∃ t : ι → Set α, (∀ i, t i ∈ f i) ∧ s = ⋂ i, t i :=
  by
  rw [← iInf_range' (g := (·))] at hs
  let ⟨_, _, V, hVs, _, _, hVU'⟩ := mem_iInf'.1 hs
  use V ∘ rangeFactorization f, fun i ↦ hVs (rangeFactorization f i)
  rw [hVU', ← rangeFactorization_surjective.iInter_comp, comp_def]

Похожие утверждения