Documentation

Analysis.Appendix_A_1

source
def Exercise_A_1_3 :
Decidable (∀ (X Y : Prop), (X → Y) → (¬X → ¬Y) → (X ↔ Y))

Exercise A.1.3.

Equations
Instances For
    source
    def Exercise_A_1_4 :
    Decidable (∀ (X Y : Prop), (X → Y) → (¬Y → ¬X) → (X ↔ Y))

    Exercise A.1.4.

    Equations
    Instances For
      source
      def Exercise_A_1_5 :
      Decidable (∀ (X Y Z : Prop), (X ↔ Y) → (Y ↔ Z) → [X, Y, Z].TFAE)

      Exercise A.1.5.

      Equations
      Instances For
        source
        def Exercise_A_1_6 :
        Decidable (∀ (X Y Z : Prop), (X → Y) → (Y → Z) → (Z → X) → [X, Y, Z].TFAE)

        Exercise A.1.6.

        Equations
        Instances For