univ_pi_eq_singleton_iff — Mathlib

English

The universal product pi univ t is a singleton {a} if and only if every t_i is a singleton {a_i}.

Русский

Универсальный произведение pi univ t является одиночкой {a} тогда и только тогда, когда каждое t_i является одиночкой {a_i}.

LaTeX

$$$$ \\pi\\mathrm{univ}\\ t = \\{a\\} \\iff \\forall i,\\ t_i = \\{a_i\\}. $$$$

Lean4

theorem univ_pi_eq_singleton_iff {a} : pi univ t = { a } ↔ ∀ i, t i = {a i} := by
  classical
  simp only [eq_singleton_iff_unique_mem]
  refine ⟨fun ⟨h₁, h₂⟩ i => ⟨by grind, fun x hx => ?_⟩, by grind⟩
  rw [← h₂ _ fun j _ => (update_mem_pi_iff_of_mem h₁).mpr (fun _ => hx) j trivial, update_self]

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