Sup_le_Sup failing to unify

Stream: general

[Connor Gordon]

When I type

import set_theory.ordinal.topology
import set_theory.cardinal.cofinality

universe u

example {A B : set ordinal.{u}} (h : A ⊆ B) : Sup A ≤ Sup B :=
begin
  apply Sup_le_Sup,
end

Lean complains to me with the error message

invalid apply tactic, failed to unify
  Sup A ≤ Sup B
with
  Sup ?m_3 ≤ Sup ?m_4
state:
A B : set ordinal,
h : A ⊆ B
⊢ Sup A ≤ Sup B

which really seems like it should be fine. Anyone have any idea what's going on?

[Eric Wieser]

When this happens a good debug strategy is to pass the arguments explicitly, as @Sup_le_Sup _ _ A B

[Connor Gordon]

Doing that gives me this:

failed to synthesize type class instance for
A B : set ordinal,
h : A ⊆ B
⊢ complete_semilattice_Sup ordinal

Unfortunately, not really sure what this means, either. Any ideas?

[Jireh Loreaux]

I don't think ordinal has (or even can have) an instance of this type class because there is no \top element for ordinals. So it seems like it's impossible to apply this particular lemma.

[Jireh Loreaux]

However, there is this: docs#ordinal.conditionally_complete_linear_order_bot, so you should be able to apply lemmas about conditionally complete lattices (or linear orders)

[Jireh Loreaux]

E.g. docs#cSup_le_cSup

[Connor Gordon]

Ah, that would do it! All that remains now is to verify that my sets are bounded above (which they are, because they're sets of ordinals). Does anyone know if there's a simple way to show that (ideally something already in the library?)

[Jireh Loreaux]

My point is set.univ : set ordinal.{u} is not bounded above. So not all sets of ordinals are bounded above.

[Connor Gordon]

But that's not a set; it's a proper class. Unless Lean does not mean what I think it does when it says set.

[Connor Gordon]

oh wait, that's the difference between set and a ZFC Set, isn't it? Any Set of ordinals is bounded above, but a set of ordinals is not necessarily?

[Connor Gordon]

It's not too important for my purposes; I just wanted to take the easy way out rather than actually prove something is bounded above. I can do it, though.

[Junyan Xu]

docs#Set is for building a model of ZFC in Lean's type theory to show (one direction) of their equiconsistency (caveat: needs inaccessible cardinals for the other direction). It's not designed for doing normal mathematics.

[Junyan Xu]

Notice that ordinal.{u} is in the universe Type (u+1) so set ordinal.{u} is also in that universe, whereas if you have a type T : Type u then set T : Type u as well.

[Junyan Xu]

Notice also that a set is definitionally the same as a predicate, so yes it may specify what you would consider proper classes, as well as sets.

[Junyan Xu]

If your set ordinal.{u} is indexed by some type in Type u, then you may use docs#ordinal.sup to get well-behaved supremum.

[Eric Wieser]

docs#ordinal.sup is just an alias for docs#supr

[Patrick Johnson]

Jireh Loreaux said:

My point is set.univ : set ordinal.{u} is not bounded above. So not all sets of ordinals are bounded above.

Well, it's not bdd_above, but whether it's bounded above in mathematical sense is debatable. Lean's definition of upper bound is

def upper_bounds (s : set α) : set α := { x | ∀ ⦃a⦄, a ∈ s → a ≤ x }

If we regard types as sets and Sort universes as Grothendieck universes, then set.univ : set ordinal.{u} is bounded above, because there are bigger ordinals that are not in Type (u+1) and the definition of upper_bounds is constrained just to type ordinal.{u} and hence incomplete. Type theory cannot accurately represent that a set is "bounded above".

[Jireh Loreaux]

Sure, I was explaining why these lemmas can't be used.