English
Two filters with HasBasis descriptions equal if and only if their bases coincide up to refinements of basis elements.
Русский
Два фильтра с базисными описаниями равны тогда, когда их базисы совпадают по включениям элементов базиса.
LaTeX
$$ext (hl : l.HasBasis p s) (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 = l'$$
Lean4
theorem ext (hl : l.HasBasis p s) (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 = l' :=
by
apply le_antisymm
· rw [hl.le_basis_iff hl']
simpa using h'
· rw [hl'.le_basis_iff hl]
simpa using h
