map_fst_prod — Mathlib

English

If g is nontrivial, then map fst (f × g) = f.

Русский

Если g ненулевой, то отображение fst от произведения фильтров равно f.

LaTeX

$$$\text{(NeBot } g) \Rightarrow \mathrm{map}\, \mathrm{Prod.fst}\ (f \times g) = f$$$

Lean4

@[simp]
theorem map_fst_prod (f : Filter α) (g : Filter β) [NeBot g] : map Prod.fst (f ×ˢ g) = f :=
  by
  ext s
  simp only [mem_map, mem_prod_iff_left, mem_preimage, eventually_const, ← subset_def, exists_mem_subset_iff]

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