preimage_apply_01_prod — Mathlib

English

Embeddings from a singleton type are in bijection with elements of the target type.

Русский

Вложения из единичного типа образуют биекцию с элементами целевого типа.

LaTeX

$$$(\\alpha \\hookrightarrow \\beta) \\cong \\beta$$$

Lean4

theorem preimage_apply_01_prod {α : Fin 2 → Type u} (s : Set (α 0)) (t : Set (α 1)) :
    (fun f : ∀ i, α i => (f 0, f 1)) ⁻¹' s ×ˢ t = Set.pi Set.univ (Fin.cons s <| Fin.cons t finZeroElim) :=
  by
  ext f
  simp [Fin.forall_fin_two]

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