English
If l has a basis {s_i} and P is a monotone property with respect to inclusion, then existence of some s with membership in l and having P(s) is equivalent to the existence of some i with p i and P(s_i).
Русский
Если l имеет базис {s_i} и P - монотонное свойство по включению, то существование некоторого s с прису́тствием в l и выполнением P(s) эквивалентно существованию некоторого i с p i и P(s_i).
LaTeX
$$$l\text{ HasBasis } p s \;\Rightarrow\; (\exists s\in l, P s) \Leftrightarrow \exists i, p i \wedge P(s i)$$$
Lean4
theorem exists_iff (hl : l.HasBasis p s) {P : Set α → Prop} (mono : ∀ ⦃s t⦄, s ⊆ t → P t → P s) :
(∃ s ∈ l, P s) ↔ ∃ i, p i ∧ P (s i) :=
⟨fun ⟨_s, hs, hP⟩ =>
let ⟨i, hi, his⟩ := hl.mem_iff.1 hs
⟨i, hi, mono his hP⟩,
fun ⟨i, hi, hP⟩ => ⟨s i, hl.mem_of_mem hi, hP⟩⟩
