Symmetric rational neighborhood relations

Content created by Egbert Rijke, Fredrik Bakke, Louis Wasserman and malarbol.

Created on 2025-08-18.
Last modified on 2026-05-02.

module metric-spaces.symmetric-rational-neighborhood-relations where

open import elementary-number-theory.positive-rational-numbers

open import foundation.binary-relations
open import foundation.dependent-products-propositions
open import foundation.function-types
open import foundation.propositions
open import foundation.universe-levels

open import metric-spaces.rational-neighborhood-relations

Idea

A rational neighborhood relation is symmetric^¶ if all ε-neighborhoods are symmetric binary relations.

Definitions

The property of being a symmetric rational neighborhood relation

module _
  {l1 l2 : Level} {A : UU l1} (B : Rational-Neighborhood-Relation l2 A)
  where

  is-symmetric-prop-Rational-Neighborhood-Relation : Prop (l1 ⊔ l2)
  is-symmetric-prop-Rational-Neighborhood-Relation =
    Π-Prop ℚ⁺ (is-symmetric-prop-Relation-Prop ∘ B)

  is-symmetric-Rational-Neighborhood-Relation : UU (l1 ⊔ l2)
  is-symmetric-Rational-Neighborhood-Relation =
    type-Prop is-symmetric-prop-Rational-Neighborhood-Relation

  is-prop-is-symmetric-Rational-Neighborhood-Relation :
    is-prop is-symmetric-Rational-Neighborhood-Relation
  is-prop-is-symmetric-Rational-Neighborhood-Relation =
    is-prop-type-Prop is-symmetric-prop-Rational-Neighborhood-Relation

Recent changes

• 2026-05-02. Fredrik Bakke and Egbert Rijke. Remove dependency between BUILTIN and postulates (#1373).
• 2025-08-18. malarbol and Louis Wasserman. Refactor metric spaces (#1450).