class ClosedUnderDicotic {G : Type (u + 1)} [Form G] (IsAmbient A : G → Prop) : Prop

• 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}

@[reducible, inline]

abbrev ClosedUnderLongDicotic {G : Type (u + 1)} [Form G] (A : G → Prop) : Prop

Equations

• ClosedUnderLongDicotic A = ClosedUnderDicotic Form.IsLong A

@[reducible, inline]

abbrev ClosedUnderShortDicotic {G : Type (u + 1)} [Form G] (A : G → Prop) : Prop

Equations

• ClosedUnderShortDicotic A = ClosedUnderDicotic Form.IsShort A

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

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

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

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

@[reducible, inline]

noncomputable abbrev Form.ClosedUnderAdd.closureOperator {G : Type (u + 1)} [Form G] : ClosureOperator (G → Prop)

The closure operator for finding the smallest additively closed set containing the given set.

Equations

• Form.ClosedUnderAdd.closureOperator = ClosureOperator.ofCompletePred (fun (A : G → Prop) => Form.ClosedUnderAdd A) ⋯

@[reducible, inline]

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

The additive closure of a given set.

Equations

• Form.ClosedUnderAdd.closure A = Form.ClosedUnderAdd.closureOperator A

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

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

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

theorem Form.ClosedUnderAdd.add_mem_closure {G : Type (u + 1)} [Form G] {A : G → Prop} {g h : G} (hg : closure A g) (hh : closure A h) : closure A (g + h)

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

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

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

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

@[reducible, inline]

noncomputable abbrev Form.Hereditary.closureOperator {G : Type (u + 1)} [Form G] : ClosureOperator (G → Prop)

The closure operator for finding the smallest hereditary set containing the given set.

Equations

• Form.Hereditary.closureOperator = ClosureOperator.ofCompletePred (fun (A : G → Prop) => Form.Hereditary A) ⋯

@[reducible, inline]

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

The hereditary closure of a given set.

Equations

• Form.Hereditary.closure A = Form.Hereditary.closureOperator A

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

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

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

theorem Form.Hereditary.has_option_mem_closure {G : Type (u + 1)} [Form G] {A : G → Prop} {g g' : G} (hg : closure A g) (h : IsOption g' g) : closure A g'

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

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

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

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

@[reducible, inline]

noncomputable abbrev Form.ClosedUnderNeg.closureOperator {G : Type (u + 1)} [Form G] : ClosureOperator (G → Prop)

The closure operator for finding the smallest conjugate closed set containing the given set.

Equations

• Form.ClosedUnderNeg.closureOperator = ClosureOperator.ofCompletePred (fun (A : G → Prop) => Form.ClosedUnderNeg A) ⋯

@[reducible, inline]

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

The conjugate closure of a given set.

Equations

• Form.ClosedUnderNeg.closure A = Form.ClosedUnderNeg.closureOperator A

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

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

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

theorem Form.ClosedUnderNeg.neg_mem_closure {G : Type (u + 1)} [Form G] {A : G → Prop} {g : G} (hg : closure A g) : closure A (-g)

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

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

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

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

@[reducible, inline]

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

The closure operator for finding the smallest dicotically closed set (given the ambient context) containing the given set.

Equations

• ClosedUnderDicotic.closureOperator IsAmbient = ClosureOperator.ofCompletePred (fun (A : G → Prop) => ClosedUnderDicotic IsAmbient A) ⋯

@[reducible, inline]

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

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

Equations

• ClosedUnderDicotic.closure IsAmbient A = (ClosedUnderDicotic.closureOperator IsAmbient) A

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

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

instance ClosedUnderDicotic.closure_closed {G : Type (u + 1)} [Form G] (IsAmbient A : G → Prop) : ClosedUnderDicotic IsAmbient (closure IsAmbient A)

theorem ClosedUnderDicotic.dicotic_mem_closure {G : Type (u + 1)} [Form G] {IsAmbient A : G → Prop} (B C : Set G) [Small.{u, u + 1} ↑B] [Small.{u, u + 1} ↑C] (hB : ∀ b ∈ B, closure IsAmbient A b) (hC : ∀ c ∈ C, closure IsAmbient A c) (hBne : B.Nonempty) (hCne : C.Nonempty) (hAmbient : IsAmbient !{B | C}) : closure IsAmbient A !{B | C}

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

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

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