English
If t is a subset of α and both f and g contain t, and m is InjectOn on t, then map m on the infimum over t agrees with infimum of maps.
Русский
Если t ⊆ α и f, g содержат t, и m инъективно ограничено на t, то map m на inf по t равен инфиму map.
LaTeX
$$theorem map_inf' {f g : Filter α} {m : α → β} {t : Set α} (htf : t ∈ f) (htg : t ∈ g) (h : InjOn m t) :
map m (f ⊓ g) = map m f ⊓ map m g$$
Lean4
theorem map_inf' {f g : Filter α} {m : α → β} {t : Set α} (htf : t ∈ f) (htg : t ∈ g) (h : InjOn m t) :
map m (f ⊓ g) = map m f ⊓ map m g := by
lift f to Filter t using htf; lift g to Filter t using htg
replace h : Injective (m ∘ ((↑) : t → α)) := h.injective
simp only [map_map, ← map_inf Subtype.coe_injective, map_inf h]
