induction over a finite set

Stream: new members

[Yoh Tanimoto]

Hello!
How can one do an induction over a finite set, say 1 ≤ m ≤ nfor a fixed n : ℕ?
I could take m and impose m ≤ n, but is there a canonical way? Specifically, I would like to prove the following.

import Mathlib
open BigOperators

variable (n : ℕ)
def f : (Fin n → C(ℝ, ℝ)) → Fin n → C(ℝ, ℝ) := fun g i => (∏ j in {l : Fin n | l.1 < i.1}.toFinset, (1 - g j)) * g i

example {n : ℕ} {g : Fin n → C(ℝ, ℝ)} (m : ℕ) (hm : m < n) :
    (∑ j in {l : Fin n | l.1 ≤ m}.toFinset, (f n g) j) = 1 - (∏ j in {l : Fin n | l.1 ≤ m - 1}.toFinset, (1 - g j)) := by
  induction' m with m ihm
  · sorry
  · sorry

[Kevin Buzzard]

My first thought on seeing this question is that you have a natural subtraction m-1 in it which is always going to make your life harder. Are you sure that your m shouldn't be renumbered so it's m+1? My second thought is that the Fin n's are also probably making your life more difficult. Are you sure you can't just have functions g indexed by the naturals (for example taking junk values like 0 for indices bigger than n)? Then you can replace Fin n with Nat and use Finset.range m with all its API instead of this finite subset of a finite type stuff. In short, I'm wondering whether you're asking the right question. Why do you need this? There might be a better way to set things up.

[Yoh Tanimoto]

Thank you for your reply!

• that is absolutely true, I should renumber m to m+1.
• I think filling the indices bigger than n is not very convenient, because this lemma will be used to show the finite subadditivity of Riesz content rieszContentAux , but I am using the definition of Rudin (for an open V it is sup {Λ f} where supp f ⊆ V and 0 ≤ f x ≤ 1).
• this specific lemma is a part of the following generalization of Urysohn's lemma.

import Mathlib

open BigOperators Function Set

lemma exists_forall_tsupport_iUnion_one_iUnion_of_isOpen_isClosed {X : Type*} [TopologicalSpace X] [NormalSpace X] [T2Space X]
    [LocallyCompactSpace X] {n : ℕ} {t : Set X} {s : Fin n → Set X}
    (hs : ∀ (i : Fin n), IsOpen (s i))
    (ht : IsClosed t) (htcp : IsCompact t) (hst : t ⊆ ⋃ i, s i) :
    ∃ f : Fin n → C(X, ℝ), (∀ (i : Fin n), tsupport (f i) ⊆ s i) ∧ EqOn (∑ i, f i) 1 t
    ∧ ∀ (i : Fin n), ∀ (x : X), f i x ∈ Icc (0 : ℝ) 1 := by
  sorry