English
If l.HasBasis p s, and there is a way to refine to p',s' using p' and s', and l contains s' elements, then l.HasBasis p' s'.
Русский
Если у l есть базис p,s и есть способ перейти к p',s' с помощью p',s', и если все s' элементы лежат в l, то 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 s' i' \in l) \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' → s' i' ∈ l) :
l.HasBasis p' s' :=
by
refine ⟨fun t => ⟨fun ht => ?_, fun ⟨i', hi', ht⟩ => mem_of_superset (h' i' hi') ht⟩⟩
rcases hl.mem_iff.1 ht with ⟨i, hi, ht⟩
rcases h i hi with ⟨i', hi', hs's⟩
exact ⟨i', hi', hs's.trans ht⟩
