exists_mem_filter_basis_of_disjoint

English

Let I be a finite index set. For each i in I, l_i is a filter on α with a basis (p_i, s_i). If the family (l_i) is pairwise disjoint, then there exists ind : ∀ i, ι i such that ∀ i, p_i(ind i) and the family {s_i(ind i)} is pairwise disjoint.

Русский

Пусть I — конечный индексный множитель. Для каждого i∈I фильтр l_i на α имеет базис (p_i, s_i). Если семейство фильтров l_i попарно взаимно непересекается, то существует отображение выбора ind i для каждого i, такое что ∀ i, p_i(ind i) и множества s_i(ind i) попарно непересекаются.

LaTeX

$$$\exists ind : \forall i, ι i,\ (\forall i, p i (ind i)) \land \mathrm{Pairwise}(\mathrm{Disjoint\ on}\ (\lambda i.\ s i (ind i))).$$$

Lean4

theorem _root_.Pairwise.exists_mem_filter_basis_of_disjoint {I} [Finite I] {l : I → Filter α} {ι : I → Sort*}
    {p : ∀ i, ι i → Prop} {s : ∀ i, ι i → Set α} (hd : Pairwise (Disjoint on l)) (h : ∀ i, (l i).HasBasis (p i) (s i)) :
    ∃ ind : ∀ i, ι i, (∀ i, p i (ind i)) ∧ Pairwise (Disjoint on fun i => s i (ind i)) :=
  by
  rcases hd.exists_mem_filter_of_disjoint with ⟨t, htl, hd⟩
  choose ind hp ht using fun i => (h i).mem_iff.1 (htl i)
  exact ⟨ind, hp, hd.mono fun i j hij => hij.mono (ht _) (ht _)⟩

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