Projective sets, intuitionistically

by Veldman

Definition 29 gives two inductive conditions (i),(ii) for membership in a set CB. Condition (iii) states that all members of CB are given by (i) and (ii). Here we prove that an analogue of (iii) holds in Lean's inductive type theory, using the cases tactic.

inductive veldman : Type

• i: veldman → veldman
• ii: veldman → veldman

theorem iii (x : veldman) : ∃ (y : veldman), x = y.i ∨ x = y.ii

inductive veldman₀ (α : Type) (β : Type) : Type

• i: {α β : Type} → α → veldman₀ α β
• ii: {α β : Type} → β → veldman₀ α β

theorem iii₀ {α : Type} {β : Type} (x : veldman₀ α β) : (∃ (y : α), x = veldman₀.i y) ∨ ∃ (y : β), x = veldman₀.ii y

theorem intcases (x : ℤ) : x ≤ 0 ∨ 1 ≤ x

inductive my_type : Type

• bob: my_type
• alice: my_type
• charlie: my_type

theorem cases3 (dave : my_type) : dave = my_type.bob ∨ dave = my_type.alice ∨ dave = my_type.charlie

structure royale_high : Type

• bobby : my_type

inductive bff_high : Type

• foo: bff_high
• bff: bff_high → bff_high

inductive bff_h : Type

• bff: bff_h → bff_h

theorem bff_h_none (x : bff_h) : ∃ (y : bff_h), x = y.bff

theorem bff_injective (x : bff_high) (y : bff_high) (h : x.bff = y.bff) : x = y

theorem bff_iii (x : bff_high) : x = bff_high.foo ∨ ∃ (y : bff_high), x = y.bff