English
Two filters with equivalent HasBasis descriptions are equal if they agree on inclusions of basis elements.
Русский
Два фильтра с эквивалентными описаниями HasBasis равны, если они согласуются по включениям базисных элементов.
LaTeX
$$ext (hl : l.HasBasis p s) (hl' : l'.HasBasis p' s') (...) : l = l'$$
Lean4
/-- If `{s i | p i}` is a basis of a filter `l` and each `s i` includes `s j` such that
`p j ∧ q j`, then `{s j | p j ∧ q j}` is a basis of `l`. -/
theorem restrict (h : l.HasBasis p s) {q : ι → Prop} (hq : ∀ i, p i → ∃ j, p j ∧ q j ∧ s j ⊆ s i) :
l.HasBasis (fun i => p i ∧ q i) s :=
by
refine ⟨fun t => ⟨fun ht => ?_, fun ⟨i, hpi, hti⟩ => h.mem_iff.2 ⟨i, hpi.1, hti⟩⟩⟩
rcases h.mem_iff.1 ht with ⟨i, hpi, hti⟩
rcases hq i hpi with ⟨j, hpj, hqj, hji⟩
exact ⟨j, ⟨hpj, hqj⟩, hji.trans hti⟩
