map_congr — Mathlib

English

If m1 and m2 are equal eventually, their maps coincide: map m1 f = map m2 f.

Русский

Если m1 и m2 равны в пределе, их отображения совпадают: map m1 f = map m2 f.

LaTeX

$$map_congr {m₁ m₂ : α → β} {f : Filter α} (h : m₁ =ᶠ[f] m₂) : map m₁ f = map m₂ f$$

Lean4

/-- If functions `m₁` and `m₂` are eventually equal at a filter `f`, then
they map this filter to the same filter. -/
theorem map_congr {m₁ m₂ : α → β} {f : Filter α} (h : m₁ =ᶠ[f] m₂) : map m₁ f = map m₂ f :=
  Filter.ext' fun _ => eventually_congr (h.mono fun _ hx => hx ▸ Iff.rfl)

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