Documentation

Foundation.Logic.Disjunctive

class LO.System.Disjunctive {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] (𝓒 : S) :
Instances
    theorem LO.System.disjunctive {F : Type u_1} {inst✝ : LO.LogicalConnective F} {S : Type u_2} {inst✝¹ : LO.System F S} {𝓒 : S} [self : LO.System.Disjunctive 𝓒] {Ο† ψ : F} :
    𝓒 ⊒! Ο† β‹Ž ψ β†’ 𝓒 ⊒! Ο† ∨ 𝓒 ⊒! ψ

    Alias of LO.System.Disjunctive.disjunctive.

    theorem LO.System.iff_disjunctive {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓒 : S} :
    LO.System.Disjunctive 𝓒 ↔ βˆ€ {Ο† ψ : F}, 𝓒 ⊒! Ο† β‹Ž ψ β†’ 𝓒 ⊒! Ο† ∨ 𝓒 ⊒! ψ