English
If the index set is effectively constrained by a predicate p, and this predicate is satisfied for some index, then map distributes over the conditional infimum.
Русский
Если индексный набор ограничен условием p и существует индекс, удовлетворяющий p, тогда map распределяется по условному inf.
LaTeX
$$map_biInf_eq {ι : Type w} {f : ι → Filter α} {m : α → β} {p : ι → Prop} (h : DirectedOn (f ⁻¹'o (· ≥ ·)) {x | p x}) (ne : ∃ i, p i) :
map m (⨅ (i) (_ : p i), f i) = ⨅ (i) (_ : p i), map m (f i)$$
Lean4
theorem map_biInf_eq {ι : Type w} {f : ι → Filter α} {m : α → β} {p : ι → Prop}
(h : DirectedOn (f ⁻¹'o (· ≥ ·)) {x | p x}) (ne : ∃ i, p i) :
map m (⨅ (i) (_ : p i), f i) = ⨅ (i) (_ : p i), map m (f i) :=
by
haveI := nonempty_subtype.2 ne
simp only [iInf_subtype']
exact map_iInf_eq h.directed_val
