restrict_subset — Mathlib

English

If l has basis p s and V ∈ l, then l has basis p i ∧ s i ⊆ V with the same s.

Русский

Если у фильтра есть базис p s и V ∈ l, то существует базис с тем же s, но пометкой s i ⊆ V.

LaTeX

$$restrict_subset (h : l.HasBasis p s) {V : Set α} (hV : V ∈ l) : l.HasBasis (fun i => p i ∧ s i ⊆ V) s$$

Lean4

/-- If `{s i | p i}` is a basis of a filter `l` and `V ∈ l`, then `{s i | p i ∧ s i ⊆ V}`
is a basis of `l`. -/
theorem restrict_subset (h : l.HasBasis p s) {V : Set α} (hV : V ∈ l) : l.HasBasis (fun i => p i ∧ s i ⊆ V) s :=
  h.restrict fun _i hi =>
    (h.mem_iff.1 (inter_mem hV (h.mem_of_mem hi))).imp fun _j hj => ⟨hj.1, subset_inter_iff.1 hj.2⟩

Похожие утверждения