class Cslib.Logic.LogicalEquivalence (Proposition : Type u) [HasContext Proposition] (Judgement : Type v) [HasHContext Judgement Proposition] (Valid : Judgement → Sort w) : Sort (max (max (u + 1) (u_2 + 1)) w)

A logical equivalence for a given type of Judgements is a congruence on propositions that preserves validity of judgements under any judgemental context.

• eqv (a b : Proposition) : Prop

  The logical equivalence relation.

• congruence : Congruence Proposition (eqv Valid)

  Proof that eqv is a congruence.

• eqv_fill_valid {a b : Proposition} (heqv : eqv Valid a b) (c : HasHContext.Context Judgement Proposition) (h : Valid c<[a]) : Valid c<[b]

  Validity is preserved for any judgemental context.

def Cslib.Logic.«term_≡_» : Lean.TrailingParserDescr

The logical equivalence relation.

Equations

• Cslib.Logic.«term_≡_» = Lean.ParserDescr.trailingNode `Cslib.Logic.«term_≡_» 29 30 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≡ ") (Lean.ParserDescr.cat `term 30))