English
A simplification of mem_iInf_finset that uses a trivial rearrangement of indices and sets within a Finset.
Русский
Упрощение mem_iInf_finset, использующее тривиальное переставление индексов и множеств в Finset.
LaTeX
$$$ (t ∈ \iInf fun a \in s, f a) \iff \exists p : α \to Set β, (\forall a ∈ s, p(a) ∈ f a) \land t = \bigcap_{a ∈ s} p(a) $$$
Lean4
@[elab_as_elim]
theorem iInf_sets_induct {f : ι → Filter α} {s : Set α} (hs : s ∈ iInf f) {p : Set α → Prop} (uni : p univ)
(ins : ∀ {i s₁ s₂}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)) : p s := by
classical
rw [mem_iInf_finite'] at hs
simp only [← Finset.inf_eq_iInf] at hs
rcases hs with ⟨is, his⟩
induction is using Finset.induction_on generalizing s with
| empty => rwa [mem_top.1 his]
| insert _ _ _ ih =>
rw [Finset.inf_insert, mem_inf_iff] at his
rcases his with ⟨s₁, hs₁, s₂, hs₂, rfl⟩
exact ins hs₁ (ih hs₂)
