This file contains basic properties about well-defined (bundled) properties. In particular, we show they form a complete atomic boolean algebra.

@[instance_reducible]

instance PiBase.Formal.Property.instMax : Max Property

The disjunction of two properties

Equations

• PiBase.Formal.Property.instMax = { max := fun (p q : PiBase.Formal.Property) => { toPred := p.toPred ⊔ q.toPred, well_defined := ⋯ } }

@[instance_reducible]

instance PiBase.Formal.Property.instMin : Min Property

The conjunction of two properties

Equations

• PiBase.Formal.Property.instMin = { min := fun (p q : PiBase.Formal.Property) => { toPred := p.toPred ⊓ q.toPred, well_defined := ⋯ } }

@[instance_reducible]

instance PiBase.Formal.Property.instLE : LE Property

For two properties p, q, we write p ≤ q if p is stronger than q (i.e. p implies q)

Equations

• PiBase.Formal.Property.instLE = { le := fun (p q : PiBase.Formal.Property) => p.toPred ≤ q.toPred }

@[instance_reducible]

instance PiBase.Formal.Property.instLT : LT Property

For two properties p, q, we write p < q if p is strictly stronger than q (i.e. p implies q and p ≠ q)

Equations

• PiBase.Formal.Property.instLT = { lt := fun (p q : PiBase.Formal.Property) => p.toPred < q.toPred }

@[instance_reducible]

instance PiBase.Formal.Property.instSupSet : SupSet Property

The disjunction of a family of properties is a property.

Equations

• PiBase.Formal.Property.instSupSet = { sSup := fun (𝓟 : Set PiBase.Formal.Property) => { toPred := ⨆ p ∈ 𝓟, p.toPred, well_defined := ⋯ } }

@[instance_reducible]

instance PiBase.Formal.Property.instInfSet : InfSet Property

The conjunction of a family of properties is a property.

Equations

• PiBase.Formal.Property.instInfSet = { sInf := fun (𝓟 : Set PiBase.Formal.Property) => { toPred := ⨅ p ∈ 𝓟, p.toPred, well_defined := ⋯ } }

@[instance_reducible]

instance PiBase.Formal.Property.instTop : Top Property

The "weakest" property (which holds for all topological spaces)

Equations

• PiBase.Formal.Property.instTop = { top := { toPred := ⊤, well_defined := ⋯ } }

@[instance_reducible]

instance PiBase.Formal.Property.instBot : Bot Property

The "strongest" property (which holds for no topological spaces)

Equations

• PiBase.Formal.Property.instBot = { bot := { toPred := ⊥, well_defined := @PiBase.Formal.Property.instBot._proof_1 } }

@[instance_reducible]

instance PiBase.Formal.Property.instCompl : Compl Property

For a property p, we write pᶜ for its negation.

Equations

• PiBase.Formal.Property.instCompl = { compl := fun (p : PiBase.Formal.Property) => { toPred := p.toPredᶜ, well_defined := ⋯ } }

@[instance_reducible]

instance PiBase.Formal.Property.instHImp : HImp Property

Equations

• PiBase.Formal.Property.instHImp = { himp := fun (p q : PiBase.Formal.Property) => { toPred := p.toPred ⇨ q.toPred, well_defined := ⋯ } }

@[instance_reducible]

instance PiBase.Formal.Property.instHNot : HNot Property

Equations

• PiBase.Formal.Property.instHNot = { hnot := fun (p : PiBase.Formal.Property) => { toPred := ￢p.toPred, well_defined := ⋯ } }

@[instance_reducible]

instance PiBase.Formal.Property.instSDiff : SDiff Property

Equations

• PiBase.Formal.Property.instSDiff = { sdiff := fun (p q : PiBase.Formal.Property) => { toPred := p.toPred \ q.toPred, well_defined := ⋯ } }

@[instance_reducible]

instance PiBase.Formal.Property.instCompleteAtomicBooleanAlgebra : CompleteAtomicBooleanAlgebra Property

(Well-defined) properties naturally form a complete atomatic boolean algebra

Equations

• One or more equations did not get rendered due to their size.