inf_principal — Mathlib

English

The infimum of a filter l with a principal filter 𝓟 s has a basis given by s_i ∩ s for each i.

Русский

Радиус инфинум фильтра l с принципиальным фильтром 𝓟 s имеет базис, состоящий из s_i ∩ s.

LaTeX

$$$\\text{HasBasis}(l \\inf \\mathcal{P} s)\\left(\\lambda i: s(i) \\cap s\\right)$$$

Lean4

theorem inf_principal (hl : l.HasBasis p s) (s' : Set α) : (l ⊓ 𝓟 s').HasBasis p fun i => s i ∩ s' :=
  ⟨fun t => by simp only [mem_inf_principal, hl.mem_iff, subset_def, mem_setOf_eq, mem_inter_iff, and_imp]⟩

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