English
There is a unique GoodProduct for the singleton false function.
Русский
Единственность GoodProduct для единственного false.
LaTeX
$$$$\\text{Unique}\\;\\{ l \\;|\\; \\mathrm{Products.isGood}(\\{\\mathrm{false}\\})\\; l \\}$$$$
Lean4
/-- There is a unique `GoodProducts` for the singleton `{fun _ ↦ false}`. -/
noncomputable instance : Unique { l // Products.isGood ({fun _ ↦ false} : Set (I → Bool)) l }
where
default := ⟨Products.nil, Products.isGood_nil⟩
uniq := by
intro ⟨⟨l, hl⟩, hll⟩
ext
apply Subtype.ext
apply (List.lex_nil_or_eq_nil l (r := (· < ·))).resolve_left
intro _
apply hll
have he : { Products.nil } ⊆ {m | m < ⟨l, hl⟩} := by
simpa only [Products.nil, Products.lt_iff_lex_lt, Set.singleton_subset_iff, Set.mem_setOf_eq]
grw [← he]
rw [Products.span_nil_eq_top]
exact Submodule.mem_top
