Kuratowski’s problem in constructive Topology

FRANCESCO CIRAULO

We proved lemma 2.2 using the following formal theorems theorem_1 through theorem_10.

axiom cl_1 {α : Type} [PartialOrder α] (c : α → α) (x : α) : x ≤ c x

axiom cl_2 {α : Type} (c : α → α) (x : α) : c (c x) = c x

axiom cl_3 {α : Type} [PartialOrder α] (c : α → α) {x y : α} : x ≤ y → c x ≤ c y

axiom int_1 {α : Type} [PartialOrder α] (i : α → α) (x : α) : i x ≤ x

axiom int_2 {α : Type} (i : α → α) (x : α) : i (i x) = i x

axiom int_3 {α : Type} [PartialOrder α] (i : α → α) {x y : α} : x ≤ y → i x ≤ i y

theorem lemma_1 {α : Type} [PartialOrder α] (c i : α → α) (x : α) : i x ≤ i (c (i x))

theorem lemma_2 {α : Type} [PartialOrder α] (c i : α → α) (x : α) : i (c (i x)) ≤ i (c x)

theorem lemma_3 {α : Type} [PartialOrder α] (c i : α → α) (x : α) : i (c (i x)) ≤ c (i x)

theorem lemma_4 {α : Type} [PartialOrder α] (c i : α → α) (x : α) : i (c x) ≤ c (i (c x))

theorem lemma_5 {α : Type} [PartialOrder α] (c i : α → α) (x : α) : c (i x) ≤ c (i (c x))

theorem lemma_6 {α : Type} [PartialOrder α] (c i : α → α) (x : α) : c (i (c x)) ≤ c x

theorem lemma_7 {α : Type} [PartialOrder α] (i : α → α) (x : α) : i x ≤ id x

theorem lemma_8 {α : Type} [PartialOrder α] (c : α → α) (x : α) : id x ≤ c x

theorem lemma_A {α : Type} [PartialOrder α] (c i : α → α) (x : α) : i (c x) = i (c (i (c x)))

theorem lemma_B {α : Type} [PartialOrder α] (c i : α → α) (x : α) : c (i x) = c (i (c (i x)))

theorem theorem_1 {α : Type} [PartialOrder α] (c i : α → α) : (∀ (x : α), c (i (c x)) ≤ id x) ↔ ∀ (x : α), c (i (c x)) = i x

theorem theorem_2 {α : Type} [PartialOrder α] (c i : α → α) : (∀ (x : α), id x ≤ c (i (c x))) ↔ ∀ (x : α), c x = c (i (c x))

theorem theorem_3 {α : Type} [PartialOrder α] (c i : α → α) : ((∀ (x : α), i (c x) ≤ c (i x)) ↔ ∀ (x : α), c (i (c x)) = c (i x)) ∧ ((∀ (x : α), c (i (c x)) = c (i x)) ↔ ∀ (x : α), i (c x) = i (c (i x)))

theorem theorem_4 {α : Type} [PartialOrder α] (c i : α → α) : (∀ (x : α), i (c x) ≤ id x) ↔ ∀ (x : α), i (c x) = i x

theorem theorem_5 {α : Type} [PartialOrder α] (c i : α → α) : (∀ (x : α), id x ≤ i (c x)) ↔ ∀ (x : α), c x = i (c x)

theorem theorem_6 {α : Type} [PartialOrder α] (c i : α → α) : ((∀ (x : α), c (i x) ≤ i (c x)) ↔ ∀ (x : α), c (i (c x)) = i (c x)) ∧ ((∀ (x : α), c (i (c x)) = i (c x)) ↔ ∀ (x : α), c (i x) = i (c (i x)))

theorem theorem_7 {α : Type} [PartialOrder α] (c i : α → α) : (∀ (x : α), c (i x) ≤ id x) ↔ ∀ (x : α), c (i x) = i x

theorem theorem_8 {α : Type} [PartialOrder α] (c i : α → α) : (∀ (x : α), id x ≤ c (i x)) ↔ ∀ (x : α), c x = c (i x)

theorem theorem_9 {α : Type} [PartialOrder α] (c i : α → α) : (∀ (x : α), i (c (i x)) ≤ id x) ↔ ∀ (x : α), i (c (i x)) = i x

theorem theorem_10 {α : Type} [PartialOrder α] (c i : α → α) : (∀ (x : α), id x ≤ i (c (i x))) ↔ ∀ (x : α), c x = i (c (i x))