preimage_apply_01_prod' — Mathlib

English

The preimage of s × t under the map f ↦ (f 0, f 1) is bijective with Set.univ × Set.t via Fin(2) coordinates.

Русский

Образ предобраза под отображением f ↦ (f(0), f(1)) равен s × t и эквивалентен Set.univ × t через координаты Fin(2).

LaTeX

$$$\\{ f : \\forall i, α_i \\;|\\; f(0) \\in s, f(1) \\in t \\} = s \\times t$$$

Lean4

theorem preimage_apply_01_prod' {α : Type u} (s t : Set α) :
    (fun f : Fin 2 → α => (f 0, f 1)) ⁻¹' s ×ˢ t = Set.pi Set.univ ![s, t] :=
  @Fin.preimage_apply_01_prod (fun _ => α) s t

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