English
Given a filter f and a family S of sets with a compatibility map hmem, one may form a new filter whose sets are S and whose membership is transported via hmem.
Русский
Дан фильтр f и семейство S множеств с отображением совместимости hmem, можно построить новый фильтр, наборы которого равны S и члены перенесены через hmem.
LaTeX
$$$\text{def }\text{copy}(f,S,hmem):\text{Filter } α\text{ where sets:=S\,;\;...}$ (informalized)$$
Lean4
/-- Override `sets` field of a filter to provide better definitional equality. -/
protected def copy (f : Filter α) (S : Set (Set α)) (hmem : ∀ s, s ∈ S ↔ s ∈ f) : Filter α
where
sets := S
univ_sets := (hmem _).2 univ_mem
sets_of_superset h hsub := (hmem _).2 <| mem_of_superset ((hmem _).1 h) hsub
inter_sets h₁ h₂ := (hmem _).2 <| inter_mem ((hmem _).1 h₁) ((hmem _).1 h₂)
