English
Membership in Pi-type and in its mapped form corresponds to elementwise membership and equality relations along the fiber.
Русский
Принадлежность в Pi-типе и в его отображенной форме эквивалентна по элементарному членству и отношениям под волокном.
LaTeX
$$$f \\in \\mathrm{mem}\\ (\\mathrm{map}\\ f\\ s) \\iff \\exists a, \\exists h, \\mathrm{mem}(s,a)\\land f(a)=b$$$
Lean4
theorem mem_pi (m : Multiset α) (t : ∀ a, Multiset (β a)) (f : ∀ a ∈ m, β a) :
f ∈ pi m t ↔ ∀ (a) (h : a ∈ m), f a h ∈ t a :=
by
induction m using Multiset.induction_on with
| empty =>
have : f = Pi.empty β := funext (fun _ => funext fun h => (notMem_zero _ h).elim)
simp only [this, pi_zero, mem_singleton, true_iff]
intro _ h; exact (notMem_zero _ h).elim
| cons a m ih => ?_
simp_rw [pi_cons, mem_bind, mem_map, ih]
constructor
· rintro ⟨b, hb, f', hf', rfl⟩ a' ha'
by_cases h : a' = a
· subst h
rwa [Pi.cons_same]
· rw [Pi.cons_ne _ h]
apply hf'
· intro hf
refine ⟨_, hf a (mem_cons_self _ _), _, fun a ha => hf a (mem_cons_of_mem ha), ?_⟩
rw [Pi.cons_eta]
