English
If l.HasBasis p s, and for all i there exists i' with p' i' and s' i' ⊆ s i, and for all i' with p' i' there exists i with p i and s i ⊆ s' i', then l.HasBasis p' s'.
Русский
Если l имеет базис p,s и для каждого i существует i' с p' i' и s' i' ⊆ s i, а для каждого i' с p' i' существует i с p i и s i ⊆ s' i', то l.HasBasis p' s'.
LaTeX
$$$l.HasBasis p s \to (\forall i, p i \to \exists i', p' i' \wedge s' i' \subseteq s i) \to (\forall i', p' i' \to \exists i, p i \wedge s i \subseteq s' i') \to l.HasBasis p' s'$$$
Lean4
theorem to_hasBasis (hl : l.HasBasis p s) (h : ∀ i, p i → ∃ i', p' i' ∧ s' i' ⊆ s i)
(h' : ∀ i', p' i' → ∃ i, p i ∧ s i ⊆ s' i') : l.HasBasis p' s' :=
hl.to_hasBasis' h fun i' hi' =>
let ⟨i, hi, hss'⟩ := h' i' hi'
hl.mem_iff.2 ⟨i, hi, hss'⟩
