Lemma II.2.2

We prove Lemma II.2.2 from [Carmo and Jones 2022].

We show that Observation 5.2 is correct except that the example does not satisfy 5(e).

def CJ5a {U : Type u_1} (ob : Set U → Set (Set U)) : Prop

Equations

• CJ5a ob = ∀ (X : Set U), ∅ ∉ ob X

def CJ5b {U : Type u_1} (ob : Set U → Set (Set U)) : Prop

Equations

• CJ5b ob = ∀ (X Y Z : Set U), Z ∩ X = Y ∩ X → (Z ∈ ob X ↔ Y ∈ ob X)

def CJ5c_star {U : Type u_1} (ob : Set U → Set (Set U)) : Prop

Equations

• CJ5c_star ob = ∀ (X : Set U), ∀ β ⊆ ob X, β ≠ ∅ → ⋂₀ β ∩ X ≠ ∅ → ⋂₀ β ∈ ob X

def CJ5c_star_finite {U : Type u_1} (ob : Set U → Set (Set U)) : Prop

Equations

• CJ5c_star_finite ob = ∀ (X Y Z : Set U), Y ∈ ob X → Z ∈ ob X → X ∩ Y ∩ Z ≠ ∅ → Y ∩ Z ∈ ob X

def CJ5d {U : Type u_1} (ob : Set U → Set (Set U)) : Prop

Equations

• CJ5d ob = ∀ (X Y Z : Set U), Y ⊆ X → Y ∈ ob X → X ⊆ Z → Z \ X ∪ Y ∈ ob Z

def CJ5e {U : Type u_1} (ob : Set U → Set (Set U)) : Prop

Equations

• CJ5e ob = ∀ (X Y Z : Set U), Y ⊆ X → Z ∈ ob X → Y ∩ Z ≠ ∅ → Z ∈ ob Y

def CJ5bd {U : Type u_1} (ob : Set U → Set (Set U)) : Prop

Equations

• CJ5bd ob = ∀ (X Y Z : Set U), Y ∈ ob X ∧ X ⊆ Z → Z \ X ∪ Y ∈ ob Z

theorem bdImpliesD {U : Type u_1} (ob : Set U → Set (Set U)) (h : CJ5bd ob) : CJ5d ob

def CJ5f {U : Type u_1} (ob : Set U → Set (Set U)) : Prop

Equations

• CJ5f ob = ∀ (β : Set (Set U)), β ≠ ∅ → ∀ (X : Set U), (∀ Z ∈ β, X ∈ ob Z) → X ∈ ob (⋃₀ β)

def CJ5g {U : Type u_1} (ob : Set U → Set (Set U)) : Prop

Equations

• CJ5g ob = ∀ (X Y Z : Set U), Y ∈ ob X → Z ∈ ob Y → X ∩ Y ∩ Z ≠ ∅ → Y ∩ Z ∈ ob X

theorem bd5 {U : Type u_1} {ob : Set U → Set (Set U)} (b5 : CJ5b ob) (d5 : CJ5d ob) : CJ5bd ob

theorem implication_in_ob {U : Type u_1} {ob : Set U → Set (Set U)} (b5 : CJ5b ob) (d5 : CJ5d ob) {β : Set (Set U)} {X : Set U} (h : X ∈ ⋂₀ (ob '' β)) : {x : Set U | ∃ Z ∈ β, ⋃₀ β \ Z ∪ X = x} ⊆ ob (⋃₀ β)

theorem inter_not_empty {U : Type u_1} {ob : Set U → Set (Set U)} {β : Set (Set U)} {X : Set U} (h2 : β ≠ ∅) (h3 : ∀ Z ∈ β, X ∈ ob Z) (a5 : CJ5a ob) (b5 : CJ5b ob) : ⋂₀ {x : Set U | ∃ Z ∈ β, ⋃₀ β \ Z ∪ X = x} ∩ ⋃₀ β ≠ ∅

theorem II_2_2 {U : Type} {ob : Set U → Set (Set U)} (a5 : CJ5a ob) (b5 : CJ5b ob) (cstar5 : CJ5c_star ob) (d5 : CJ5d ob) : CJ5f ob

Lemma II.2.2 Formalized by RJ Reiff.

theorem II_2_1 {U : Type} {ob : Set U → Set (Set U)} (b5 : CJ5b ob) : CJ5d ob ↔ CJ5bd ob

Lemma II-2-1 Assuming condition (5b), the following condition below is equivalent to (5d): (5bd) if Y∈ob(X) and X⊆Z, then ((Z-X) ∪ Y) ∈ ob(Z)

theorem Observation_5_1_2 {U : Type} {ob : Set U → Set (Set U)} (b5 : CJ5b ob) (cstar5 : CJ5c_star ob) (d5 : CJ5d ob) (e5 : CJ5e ob) : CJ5g ob

The deduction of (5-g) is as follows:

From Y ∈ ob(X) deduce ((X∪Y)-X)∪Y)∈ob(X∪Y), i.e., Y∈ob(X∪Y) (take into account that X⊆(X∪Y), and use lemma II-2-1 of [2]);

Analogously, from Z∈ob(X) deduce ((X∪Y)-Y)∪Z)∈ob(X∪Y), i.e., ((X-Y)∪Z)∈ob(X∪Y);

Since X∩Y∩Z≠∅, we have that Y∩((X-Y)∪Z)∩(X∪Y) = Y∩Z ≠ ∅, and so, by condition (5-c), Y∩((X-Y)∪Z))∈ob(X∪Y), i.e., Y∩Z∈ob(X∪Y);

But then, from Y∩Z∈ob(X∪Y), X⊆(X∪Y) and X∩Y∩Z≠∅, by condition (5-e), it follows that Y∩Z∈ob(X) (as we wish to prove). (Formalized May 26, 2025.)

def observation_5_2 (X : Set (Fin 4)) : Set (Set (Fin 4))

The function ob from Carmo and Jones 2022 Observation 5.2.

Equations

• observation_5_2 X = if X ∩ {0, 1} = ∅ then {Y : Set (Fin 4) | Y ∩ X = {3}} else {Y : Set (Fin 4) | Y ⊇ {0, 1} ∩ X}

theorem ob52_a : CJ5a observation_5_2

theorem ob52_b : CJ5b observation_5_2

theorem ob52_c : CJ5c_star observation_5_2

theorem ob52_e' : ¬CJ5e observation_5_2

Surprisingly, 5(e) is NOT true despite what CJ 2022 claim. The mistake in the detailed proof supplied on Feb 2, 2022 is that we are in Case 1 and although I'll grant that Z ∩ Y ⊇ {0,1} ∩ Y, this doesn't matter since {0,1} ∩ Y = ∅.

theorem q_in : {0, 1} ∈ observation_5_2 Set.univ

theorem r_not_in : {0, 2} ∉ observation_5_2 (Set.univ \ {0, 1})

theorem ob52_g : CJ5g observation_5_2

theorem ob52_f : CJ5f observation_5_2