class Universe {G : Type (u + 1)} [Form G] (IsAmbient A : G → Prop) extends Form.ClosedUnderAdd A, Form.Hereditary A, Form.ClosedUnderNeg A, ClosedUnderDicotic IsAmbient A : Prop

• has_add (g h : G) (h_g : A g) (h_h : A h) : A (g + h)
• has_option {g g' : G} (h1 : A g) (h2 : IsOption g' g) : A g'
• neg_of {g : G} (h1 : A g) : A (-g)
• closed_dicotic (B C : Set G) [Small.{u, u + 1} ↑B] [Small.{u, u + 1} ↑C] (hB : ∀ b ∈ B, A b) (hC : ∀ c ∈ C, A c) : B.Nonempty → C.Nonempty → IsAmbient !{B | C} → A !{B | C}
• zero_mem : A 0
• isAmbient_of_mem {g : G} : A g → IsAmbient g

class LongUniverse {G : Type (u + 1)} [Form G] (A : G → Prop) extends Universe Form.IsLong A : Prop

• has_add (g h : G) (h_g : A g) (h_h : A h) : A (g + h)
• has_option {g g' : G} (h1 : A g) (h2 : IsOption g' g) : A g'
• neg_of {g : G} (h1 : A g) : A (-g)
• closed_dicotic (B C : Set G) [Small.{u, u + 1} ↑B] [Small.{u, u + 1} ↑C] (hB : ∀ b ∈ B, A b) (hC : ∀ c ∈ C, A c) : B.Nonempty → C.Nonempty → Form.IsLong !{B | C} → A !{B | C}
• zero_mem : A 0
• isAmbient_of_mem {g : G} : A g → Form.IsLong g

class ShortUniverse {G : Type (u + 1)} [Form G] (A : G → Prop) extends Universe Form.IsShort A : Prop

• has_add (g h : G) (h_g : A g) (h_h : A h) : A (g + h)
• has_option {g g' : G} (h1 : A g) (h2 : IsOption g' g) : A g'
• neg_of {g : G} (h1 : A g) : A (-g)
• closed_dicotic (B C : Set G) [Small.{u, u + 1} ↑B] [Small.{u, u + 1} ↑C] (hB : ∀ b ∈ B, A b) (hC : ∀ c ∈ C, A c) : B.Nonempty → C.Nonempty → Form.IsShort !{B | C} → A !{B | C}
• zero_mem : A 0
• isAmbient_of_mem {g : G} : A g → Form.IsShort g

instance instLongUniverseIsLong {G : Type (u + 1)} [Form G] : LongUniverse Form.IsLong

instance instShortUniverseIsShort {G : Type (u + 1)} [Form G] : ShortUniverse Form.IsShort

theorem Universe.sInf_closed {G : Type (u + 1)} [Form G] (IsAmbient : G → Prop) [Universe IsAmbient IsAmbient] {S : Set ↑(Set.Iic IsAmbient)} (hS : ∀ A ∈ S, Universe IsAmbient ↑A) : Universe IsAmbient ↑(sInf S)

An intersection of universes is a universe.

@[reducible, inline]

noncomputable abbrev Universe.closureOperator {G : Type (u + 1)} [Form G] (IsAmbient : G → Prop) [Universe IsAmbient IsAmbient] : ClosureOperator ↑(Set.Iic IsAmbient)

The closure operator for finding the universal closure of a given set (in the context of a given ambient). Sends a bounded predicate to the smallest Universe IsAmbient containing it.

Equations

• Universe.closureOperator IsAmbient = ClosureOperator.ofCompletePred (fun (A : ↑(Set.Iic IsAmbient)) => Universe IsAmbient ↑A) ⋯

@[reducible, inline]

noncomputable abbrev Universe.closureBounded {G : Type (u + 1)} [Form G] (IsAmbient : G → Prop) [Universe IsAmbient IsAmbient] (A : ↑(Set.Iic IsAmbient)) : ↑(Set.Iic IsAmbient)

The universal closure of a given set (within the context of a given ambient).

Equations

• Universe.closureBounded IsAmbient A = (Universe.closureOperator IsAmbient) A

@[reducible, inline]

noncomputable abbrev Universe.closure {G : Type (u + 1)} [Form G] (IsAmbient : G → Prop) [Universe IsAmbient IsAmbient] (A : G → Prop) (hA : A ≤ IsAmbient) : G → Prop

The universal closure of a given set (within the context of a given ambient).

Equations

• Universe.closure IsAmbient A hA = ↑(Universe.closureBounded IsAmbient ⟨A, hA⟩)

theorem Universe.subset_closure {G : Type (u + 1)} [Form G] (IsAmbient : G → Prop) [Universe IsAmbient IsAmbient] {A : G → Prop} (hA : A ≤ IsAmbient) : A ≤ closure IsAmbient A hA

theorem Universe.mem_closure_of_mem {G : Type (u + 1)} [Form G] (IsAmbient : G → Prop) [Universe IsAmbient IsAmbient] {A : G → Prop} {g : G} (hA : A ≤ IsAmbient) (hg : A g) : closure IsAmbient A hA g

theorem Universe.closure_le_ambient {G : Type (u + 1)} [Form G] (IsAmbient : G → Prop) [Universe IsAmbient IsAmbient] {A : G → Prop} (hA : A ≤ IsAmbient) : closure IsAmbient A hA ≤ IsAmbient

instance Universe.closure_universe {G : Type (u + 1)} [Form G] (IsAmbient : G → Prop) [Universe IsAmbient IsAmbient] {A : G → Prop} (hA : A ≤ IsAmbient) : Universe IsAmbient (closure IsAmbient A hA)

theorem Universe.closure_min {G : Type (u + 1)} [Form G] (IsAmbient : G → Prop) [Universe IsAmbient IsAmbient] {A B : G → Prop} (hA : A ≤ IsAmbient) (hAB : A ≤ B) [Universe IsAmbient B] : closure IsAmbient A hA ≤ B

theorem Universe.closure_le {G : Type (u + 1)} [Form G] (IsAmbient : G → Prop) [Universe IsAmbient IsAmbient] {A B : G → Prop} (hA : A ≤ IsAmbient) [Universe IsAmbient B] : closure IsAmbient A hA ≤ B ↔ A ≤ B

theorem Universe.closure_mono {G : Type (u + 1)} [Form G] (IsAmbient : G → Prop) [Universe IsAmbient IsAmbient] {A B : G → Prop} {hA : A ≤ IsAmbient} {hB : B ≤ IsAmbient} (hAB : A ≤ B) : closure IsAmbient A hA ≤ closure IsAmbient B hB

theorem Universe.iInter {G : Type (u + 1)} [Form G] {ι : Sort u_1} (IsAmbient A : ι → G → Prop) [∀ (i : ι), Universe (IsAmbient i) (A i)] : Universe (fun (g : G) => ∀ (i : ι), IsAmbient i g) fun (g : G) => ∀ (i : ι), A i g

The intersection of universes is a universe, with ambient space the intersection of the ambient spaces.

theorem Universe.iUnion_of_directed {G : Type (u + 1)} [Form G] {ι : Sort u_1} [Nonempty ι] (IsAmbient A : ι → G → Prop) [∀ (i : ι), Universe (IsAmbient i) (A i)] (h_directed : Directed (fun (P Q : (G → Prop) × (G → Prop)) => P.1 ≤ Q.1 ∧ P.2 ≤ Q.2) fun (i : ι) => (A i, IsAmbient i)) (h_options : ∀ (B C : Set G) [inst : Small.{u, u + 1} ↑B] [inst_1 : Small.{u, u + 1} ↑C], (∀ b ∈ B, ∃ (i : ι), A i b) → (∀ c ∈ C, ∃ (i : ι), A i c) → B.Nonempty → C.Nonempty → (∃ (i : ι), IsAmbient i !{B | C}) → ∃ (i : ι), (∀ b ∈ B, A i b) ∧ (∀ c ∈ C, A i c) ∧ IsAmbient i !{B | C}) : Universe (fun (g : G) => ∃ (i : ι), IsAmbient i g) fun (g : G) => ∃ (i : ι), A i g

The union of a nonempty directed family of universes is a universe, with ambient space the union of the ambient spaces.

The directedness is componentwise on the family of ordered pairs (A i, IsAmbient i). We require the hypothesis that, if the Left and Right options lie in the union, and the form from dicotic closure lies in the union of the ambient spaces, then there exists a universe containing all of the options, and whose ambient space contains the relevant form. This extra hypothesis supplies the common index needed for dicotic closure.

theorem Universe.iUnion_of_directed_of_fixed_ambient {G : Type (u + 1)} [Form G] {ι : Sort u_1} [Nonempty ι] (IsAmbient : G → Prop) (A : ι → G → Prop) [∀ (i : ι), Universe IsAmbient (A i)] (h_directed : Directed (fun (x1 x2 : G → Prop) => x1 ≤ x2) A) (h_options : ∀ (B C : Set G) [inst : Small.{u, u + 1} ↑B] [inst_1 : Small.{u, u + 1} ↑C], (∀ b ∈ B, ∃ (i : ι), A i b) → (∀ c ∈ C, ∃ (i : ι), A i c) → B.Nonempty → C.Nonempty → IsAmbient !{B | C} → ∃ (i : ι), (∀ b ∈ B, A i b) ∧ ∀ c ∈ C, A i c) : Universe IsAmbient fun (g : G) => ∃ (i : ι), A i g

A specialised version of Universe.iUnion_of_directed in which every universe has the same ambient space.

@[reducible, inline]

noncomputable abbrev LongUniverse.closure {G : Type (u + 1)} [Form G] (A : G → Prop) : G → Prop

The smallest long universe containing A.

Equations

• LongUniverse.closure A = Universe.closure Form.IsLong A ⋯

instance LongUniverse.closure_universe {G : Type (u + 1)} [Form G] (A : G → Prop) : LongUniverse (closure A)

theorem LongUniverse.closure_le {G : Type (u + 1)} [Form G] {A B : G → Prop} [LongUniverse B] : closure A ≤ B ↔ A ≤ B

@[reducible, inline]

noncomputable abbrev ShortUniverse.closure {G : Type (u + 1)} [Form G] (A : G → Prop) (hA : A ≤ Form.IsShort) : G → Prop

The smallest short universe containing A.

Equations

• ShortUniverse.closure A hA = Universe.closure Form.IsShort A hA

instance ShortUniverse.closure_universe {G : Type (u + 1)} [Form G] {A : G → Prop} (hA : A ≤ Form.IsShort) : ShortUniverse (closure A hA)

theorem ShortUniverse.closure_le {G : Type (u + 1)} [Form G] {A B : G → Prop} (hA : A ≤ Form.IsShort) [ShortUniverse B] : closure A hA ≤ B ↔ A ≤ B

theorem ShortUniverse.iUnion_of_directed {G : Type (u + 1)} [Form G] {ι : Sort u_1} [Nonempty ι] (A : ι → G → Prop) [∀ (i : ι), ShortUniverse (A i)] (h_directed : Directed (fun (x1 x2 : G → Prop) => x1 ≤ x2) A) : ShortUniverse fun (g : G) => ∃ (i : ι), A i g

The union of a nonempty directed family of short universes is a short universe.