English
An irreducible s is equivalent to the property that for every finite collection t of closed sets with s ⊆ ⋃ t, there exists z ∈ t with s ⊆ z.
Русский
Неразложимость s эквивалентна тому, что для любой конечной коллекции замкнутых множеств t, если s ⊆ ⋃ t, то существует z ∈ t с s ⊆ z.
LaTeX
$$$\mathrm{IsIrreducible}(s) \iff \forall t \in \mathrm{Finset}(\mathcal{P}(X)), (\forall z \in t, \mathrm{IsClosed}(z)) \to (s \subseteq \bigcup z) \to \exists z \in t, s \subseteq z$$$
Lean4
/-- A set is irreducible if and only if for every cover by a finite collection of closed sets, it is
contained in one of the members of the collection. -/
theorem isIrreducible_iff_sUnion_isClosed :
IsIrreducible s ↔ ∀ t : Finset (Set X), (∀ z ∈ t, IsClosed z) → (s ⊆ ⋃₀ ↑t) → ∃ z ∈ t, s ⊆ z :=
by
simp only [isIrreducible_iff_sInter]
refine ((@compl_involutive (Set X) _).toPerm _).finsetCongr.forall_congr fun {t} => ?_
simp_rw [Equiv.finsetCongr_apply, Finset.forall_mem_map, Finset.mem_map, Finset.coe_map, sUnion_image,
Equiv.coe_toEmbedding, Function.Involutive.coe_toPerm, isClosed_compl_iff, exists_exists_and_eq_and]
refine forall_congr' fun _ => Iff.trans ?_ not_imp_not
simp only [not_exists, not_and, ← compl_iInter₂, ← sInter_eq_biInter, subset_compl_iff_disjoint_right,
not_disjoint_iff_nonempty_inter]
