map₂_left — Mathlib

English

If g is NeBot, map₂ (λ x _ => x) f g equals f; i.e., the left identity holds when the right factor is nonempty.

Русский

Если g неботов, то map₂ (λ x _ => x) f g равно f; т.е. левый тождественный элемент сохраняется при условии неботовости правого фильтра.

LaTeX

$$[NeBot g] ⇒ map₂ (\lambda x _ => x) f g = f$$

Lean4

@[simp]
theorem map₂_left [NeBot g] : map₂ (fun x _ => x) f g = f := by rw [← map_prod_eq_map₂, map_fst_prod]

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