English
hull_finsetInf: hull(T, inf F id) equals a preimage of UpperSet under upperClosure of F.
Русский
hull_finsetInf: hull(T, inf F id) эквивалентно образу предобраза верхнего множества через upperClosure Ф.
LaTeX
$$$\\operatorname{hull}(T, (\\inf F\\;id)) = \\operatorname{preimage}(Subtype.val, \\operatorname{UpperSet}.coe(\\text{upperClosure}(F)))$$$
Lean4
theorem hull_finsetInf (hT : ∀ p ∈ T, InfPrime p) (F : Finset α) : hull T (inf F id) = T ↓∩ upperClosure F.toSet :=
by
rw [coe_upperClosure]
induction F using Finset.cons_induction with
|
empty =>
simp only [coe_empty, mem_empty_iff_false, iUnion_of_empty, iUnion_empty, Set.preimage_empty, inf_empty]
by_contra hf
rw [← Set.not_nonempty_iff_eq_empty, not_not] at hf
obtain ⟨x, hx⟩ := hf
exact (hT x (Subtype.coe_prop x)).1 (isMax_iff_eq_top.mpr (eq_top_iff.mpr hx))
| cons a F' _ I4 =>
simp [hull_inf hT, I4]
/- Every relative-open set of the form `T ↓∩ (↑(upperClosure F))ᶜ` for `F` finite is a relative-open
set of the form `(hull T a)ᶜ` where `a = ⨅ F`. -/
