English
Under directedness and nonemptiness, map preserves infima: map m of the infimum equals the infimum of the mapped filters.
Русский
При условии направленности и нехватки элементов, отображение сохраняет inf: map m (iInf f) = iInf (map m (f i)).
LaTeX
$$map_iInf_eq {f : ι → Filter α} {m : α → β} (hf : Directed (· ≥ ·) f) [Nonempty ι], map m (iInf f) = iInf fun i => map m (f i)$$
Lean4
theorem map_iInf_eq {f : ι → Filter α} {m : α → β} (hf : Directed (· ≥ ·) f) [Nonempty ι] :
map m (iInf f) = ⨅ i, map m (f i) :=
map_iInf_le.antisymm fun s (hs : m ⁻¹' s ∈ iInf f) =>
let ⟨i, hi⟩ := (mem_iInf_of_directed hf _).1 hs
have : ⨅ i, map m (f i) ≤ 𝓟 s := iInf_le_of_le i <| by simpa only [le_principal_iff, mem_map]
Filter.le_principal_iff.1 this
