map_lift_eq — Mathlib

English

Map distributes over lift: map m on f.lift g equals f.lift of map m with g composed with map.

Русский

Отображение м распределяет над подъемом: map m над f.lift g равно f.lift (map m ∘ g).

LaTeX

$$map m (f.lift g) = f.lift (map m \circ g)$$

Lean4

theorem map_lift_eq {m : β → γ} (hg : Monotone g) : map m (f.lift g) = f.lift (map m ∘ g) :=
  have : Monotone (map m ∘ g) := map_mono.comp hg
  Filter.ext fun s => by simp only [mem_lift_sets hg, mem_lift_sets this, mem_map, Function.comp_apply]

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