English
For a finite s, membership in the infimum iInf of a family over s is equivalent to the existence of p with p a_i ∈ f a for all a ∈ s and t the intersection of p's equals the infimum intersection.
Русский
Для конечного множества s, принадлежность в iInf семейства по s эквивалентна существованию p с p(a) ∈ f(a) для всех a ∈ s и t равенству пересечению p(a) по a ∈ s и iInf.
LaTeX
$$$ (t ∈ \iInf a \in s, f a) \iff \exists p : α \to Set β, \; (\forall a ∈ s, p(a) \in f a) \land t = \bigcap_{a \in s} p(a) $$$
Lean4
theorem mem_iInf_finset {s : Finset α} {f : α → Filter β} {t : Set β} :
(t ∈ ⨅ a ∈ s, f a) ↔ ∃ p : α → Set β, (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ a ∈ s, p a := by
classical
simp only [← Finset.set_biInter_coe, biInter_eq_iInter, iInf_subtype']
refine ⟨fun h => ?_, ?_⟩
· rcases (mem_iInf_of_finite _).1 h with ⟨p, hp, rfl⟩
refine ⟨fun a => if h : a ∈ s then p ⟨a, h⟩ else univ, fun a ha => by simpa [ha] using hp ⟨a, ha⟩, ?_⟩
refine iInter_congr_of_surjective id surjective_id ?_
rintro ⟨a, ha⟩
simp [ha]
· rintro ⟨p, hpf, rfl⟩
exact iInter_mem.2 fun a => mem_iInf_of_mem a (hpf a a.2)
