English
A subset s is preirreducible if and only if for every two closed sets z1, z2, whenever s is contained in z1 ∪ z2, then s is contained in z1 or in z2.
Русский
Подмножество s преднеразложимо тогда и только тогда, когда для любых двух замкнутых множеств z1, z2, если s ⊆ z1 ∪ z2, то s ⊆ z1 или s ⊆ z2.
LaTeX
$$$\mathrm{IsPreirreducible}(s) \iff \forall z_1,z_2, \mathrm{IsClosed}(z_1) \to \mathrm{IsClosed}(z_2) \to s \subseteq z_1 \cup z_2 \to s \subseteq z_1 \lor s \subseteq z_2$$$
Lean4
/-- A set is preirreducible if and only if
for every cover by two closed sets, it is contained in one of the two covering sets. -/
theorem isPreirreducible_iff_isClosed_union_isClosed :
IsPreirreducible s ↔ ∀ z₁ z₂ : Set X, IsClosed z₁ → IsClosed z₂ → s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂ :=
by
refine
compl_surjective.forall.trans <| forall_congr' fun z₁ => compl_surjective.forall.trans <| forall_congr' fun z₂ => ?_
simp only [isOpen_compl_iff, ← compl_union, inter_compl_nonempty_iff]
refine forall₂_congr fun _ _ => ?_
rw [← and_imp, ← not_or, not_imp_not]
