Stream: Beginner Questions

Topic: Adding sort constraint to sublocales

Ata Keskin (Apr 25 2023 at 11:49):

Hi. I am trying to define some locales to formalize martingales. I want to show that any martingale is also a submartingale. The submartingale locale has the additional sort constraint "preorder", while the martingale locale does not. Therefore I cannot simply use the sublocale command. I have wrote the statement down using

lemma martingale_is_submartingale:
  assumes "martingale M F (N :: _ :: {second_countable_topology, real_normed_vector, preorder} measure) Y"
  shows "submartingale M F N Y"

however this doesn't allow me to use unfold_locales fully, as I still have to prove all the shared axioms between the two locales manually. Ideally I would want to be able to do something like:

sublocale martingale M F "N :: _ :: {second_countable_topology, real_normed_vector, preorder} measure" Y \subseteq submartingale M F N Y for M F N Y

Is there anyway to do this?

Last updated: Apr 27 2024 at 16:16 UTC