Documentation

Init.BinderPredicates

The syntax category of binder predicates contains predicates like > 0, ∈ s, etc. (: t should not be a binder predicate because it would clash with the built-in syntax for ∀/∃.)

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

      satisfies_binder_pred% t pred expands to a proposition expressing that t satisfies pred.

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

        The notation ∃ x < 2, p x is shorthand for ∃ x, x < 2 ∧ p x, and similarly for other binary operators.

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

          The notation ∀ x < 2, p x is shorthand for ∀ x, x < 2 → p x, and similarly for other binary operators.

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

            Declare ∃ x > y, ... as syntax for ∃ x, x > y ∧ ...

            Equations
            Instances For

              Declare ∃ x ≥ y, ... as syntax for ∃ x, x ≥ y ∧ ...

              Equations
              Instances For

                Declare ∃ x < y, ... as syntax for ∃ x, x < y ∧ ...

                Equations
                Instances For

                  Declare ∃ x ≤ y, ... as syntax for ∃ x, x ≤ y ∧ ...

                  Equations
                  Instances For

                    Declare ∃ x ≠ y, ... as syntax for ∃ x, x ≠ y ∧ ...

                    Equations
                    Instances For

                      Declare ∀ x ∈ y, ... as syntax for ∀ x, x ∈ y → ... and ∃ x ∈ y, ... as syntax for ∃ x, x ∈ y ∧ ...

                      Equations
                      Instances For

                        Declare ∀ x ∉ y, ... as syntax for ∀ x, x ∉ y → ... and ∃ x ∉ y, ... as syntax for ∃ x, x ∉ y ∧ ...

                        Equations
                        Instances For

                          Declare ∀ x ⊆ y, ... as syntax for ∀ x, x ⊆ y → ... and ∃ x ⊆ y, ... as syntax for ∃ x, x ⊆ y ∧ ...

                          Equations
                          Instances For

                            Declare ∀ x ⊂ y, ... as syntax for ∀ x, x ⊂ y → ... and ∃ x ⊂ y, ... as syntax for ∃ x, x ⊂ y ∧ ...

                            Equations
                            Instances For

                              Declare ∀ x ⊇ y, ... as syntax for ∀ x, x ⊇ y → ... and ∃ x ⊇ y, ... as syntax for ∃ x, x ⊇ y ∧ ...

                              Equations
                              Instances For

                                Declare ∀ x ⊃ y, ... as syntax for ∀ x, x ⊃ y → ... and ∃ x ⊃ y, ... as syntax for ∃ x, x ⊃ y ∧ ...

                                Equations
                                Instances For