finite products from binary and unit

Stream: Is there code for X?

[Kevin Buzzard]

Do we have this?

import Mathlib

axiom IsNice (X : Type*) : Prop

namespace IsNice

section API

variable (X Y : Type*)

lemma iso (e : X ≃ Y) (hX : IsNice X) : IsNice Y := sorry

lemma unit : IsNice PUnit := sorry

lemma prod (hX : IsNice X) (hY : IsNice Y) : IsNice (X × Y) := sorry

end API

theorem pi_finite (ι : Type*) [Finite ι]
  (X : ι → Type*) (hX : ∀ i, IsNice (X i)): IsNice (∀ i, X i) :=
  sorry -- "obvious by induction"

My application is to topological modules and IsNice is a typeclass on topologies FWIW.

[Yakov Pechersky]

Induct on Nat.card iota?

[Yakov Pechersky]

And use docs#Finite.card_option with docs#Finite.card_eq

[Kevin Buzzard]

Yeah and it's going to be horrible :-(

[Kevin Buzzard]

Furthermore I've realised that this might not be enough for me unless there's a trick. In my application I only know that the predicate is preserved under homeomorphisms, so I would have to rethink how to apply tha above theory

[Markus Himmel]

Something very similar happens in category theory land in https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/CategoryTheory/Limits/Constructions/FiniteProductsOfBinaryProducts.lean and there it's not too terrible.

[Bhavik Mehta]

The idea here is to show it for ι = Fin n by induction on n, then use the fact that it's preserved by isos on ι to get it for all finite types. Hopefully the homeomorphisms you have are okay enough for this?

[Eric Wieser]

Does docs#Fintype.inductionEmptyOption help?

[Kevin Buzzard]

That's what I've been using but in practice there seems to be lots of things missing (for example the homeo between (I oplus J -> X) and (I -> X) x (J -> X))