Specifying conditions for iSup

Stream: new members

[VayusElytra]

Hello,

I am trying to right a somewhat complex condition to take a supremum over. I have the following:

structure ExampleStruct where
  ExampleField : Type

structure Substructure where
  S : Set (ExampleStruct)

instance : CompleteLattice ExampleStruct := by
  sorry

variable {Z : ExampleStruct} in
lemma ExLemma (I : Substructure) (J : Substructure) (d : I.S → Set (ExampleStruct))
  (h : (∀ (N : I.S), d N ⊆ J.S)) : Z = _ := sorry

Instead of Z = _ (placeholder), I would like to express Z = ⨆ (A : J.S, ∃ B : I.S, A ∈ d B), A, so Z is the supremum of all the elements of J.S that are also in the image of some B in I.S. This wording does not please Lean, and Mathlib.Order.CompleteLattice does not give documentation for writing more complex supremums like this.

What is the proper way to write this expression? I am thinking I could maybe just define a large set X to be the union of d B for all B, and then simply take the supremum for A in X, but that sounds like it would lead me away from API.

[Edward van de Meent]

one way is to take a nested supremum, where the inner supremum is over the proofs that the condition holds, i.e. something like this: ⨆ (A : J.S), ⨆ (_:∃ B : I.S, A ∈ d B), A (which i think may even simplify to ⨆ (A : J.S), ⨆ (B : I.S),⨆ (_: A ∈ d B), A in this case). if you don't like the nestedness, you could opt for taking the supremum of ⨆ ( A' : {A : J.S // ∃ B : I.S, A ∈ d B}), A'.val

[VayusElytra]

Thank you! I think that should work really well.

I'll add one more question that feels very stupid and doesn't deserve to make an entirely new discussion on: in the same context, I have:

variable {K : Type} [DivisionRing K] (Z : ModuleCat K)
variable {A B : Submodule K Z} [Inhabited B]
lemma LT_of_submod : A < A ⊔ B := sorry

I was looking through the documentation of Submonoid to find if there was some theorem that would give me this result instantly, but I could not find one. Is there a trivial way of doing this?

[Kevin Buzzard]

Is it true? What if A=B?

[VayusElytra]

You're right of course; I need to specify that the setting I am in, these submodules are embedded into Z differently, so they cannot be equal to or included in each other. I think I need to review my implementation in a bit more detail before I work on this, thank you.

[Kevin Buzzard]

Maybe you want to prove it under the assumption that there's an element of Z which is in B but not A.