Symmetric premetric structures on types

Content created by Fredrik Bakke and malarbol.

Created on 2024-09-28.
Last modified on 2024-09-28.

module metric-spaces.symmetric-premetric-structures where
Imports 
open import elementary-number-theory.positive-rational-numbers

open import foundation.binary-relations
open import foundation.existential-quantification
open import foundation.function-types
open import foundation.identity-types
open import foundation.propositions
open import foundation.universe-levels

open import metric-spaces.premetric-structures

Idea

A premetric is symmetric if d-neighborhoods are symmetric for all positive rational numbers d. I.e., upper bounds on the distance between two elements x and y in a symmetric premetric are also upper bounds on the distance between y and x.

Definitions

The property of being a symmetric premetric structure

module _
  {l1 l2 : Level} {A : UU l1} (B : Premetric l2 A)
  where

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

  is-symmetric-Premetric : UU (l1 ⊔ l2)
  is-symmetric-Premetric = type-Prop is-symmetric-prop-Premetric

  is-prop-is-symmetric-Premetric : is-prop is-symmetric-Premetric
  is-prop-is-symmetric-Premetric =
    is-prop-type-Prop is-symmetric-prop-Premetric

Properties

Indistiguishability in a symmetric premetric is symmetric

module _
  {l1 l2 : Level} {A : UU l1} (B : Premetric l2 A)
  (S : is-symmetric-Premetric B)
  where

  is-symmetric-is-indistinguishable-is-symmetric-Premetric :
    is-symmetric (is-indistinguishable-Premetric B)
  is-symmetric-is-indistinguishable-is-symmetric-Premetric x y H d =
    S d x y (H d)

The separatedness relation in a symmetric premetric is symmetric

module _
  {l1 l2 : Level} {A : UU l1} (B : Premetric l2 A)
  (S : is-symmetric-Premetric B)
  where

  is-symmetric-is-separated-pt-is-symmetric-Premetric :
    is-symmetric (is-separated-pt-Premetric B)
  is-symmetric-is-separated-pt-is-symmetric-Premetric x y =
    elim-exists
      ( is-separated-pt-prop-Premetric B y x)
      ( λ d I → intro-exists d (I ∘ S d y x))

Recent changes