English
If a filter l has a basis {s_i} indexed by i in I with property p i, and we replace each basis set s_i by a subset t_i ⊆ s_i that still belongs to l whenever p i holds, then the family {t_i} also forms a basis for l with the same index set.
Русский
Если фильтр l имеет базис {s_i}, индексируемый по i из I, удовлетворяющий условию p i, и если заменить каждый базисный элемент s_i на подмножество t_i ⊆ s_i, которое по-прежнему принадлежит l при выполнении p_i, тогда семейство {t_i} тоже образует базис для l с тем же индексом.
LaTeX
$$$l\text{ имеет базис } p s\quad\Rightarrow\quad (\forall i,\ p i \Rightarrow t i \subseteq s i) \land (\forall i,\ p i \Rightarrow t i \in l) \Rightarrow l\text{ имеет базис } p t$$
Lean4
theorem to_subset (hl : l.HasBasis p s) {t : ι → Set α} (h : ∀ i, p i → t i ⊆ s i) (ht : ∀ i, p i → t i ∈ l) :
l.HasBasis p t :=
hl.to_hasBasis' (fun i hi => ⟨i, hi, h i hi⟩) ht
