Height bounds for every finite upper set

theorem MagnitudeConjecture.UpperSetHeight.card_difference_le_height_difference {T : Type u} [PartialOrder T] [Fintype T] (height : Finset T → ℕ) (hstep : ∀ (U V : Finset T), IsUpperSet ↑U → IsUpperSet ↑V → U ⊂ V → height U < height V) (U V : Finset T) (hU : IsUpperSet ↑U) (hV : IsUpperSet ↑V) (hUV : U ⊆ V) : height U + V.card ≤ height V + U.card

A strictly increasing height on upper sets rises by at least the number of elements added between any two upper sets.

theorem MagnitudeConjecture.UpperSetHeight.height_eq_card {T : Type u} [PartialOrder T] [Fintype T] (height : Finset T → ℕ) (hstep : ∀ (U V : Finset T), IsUpperSet ↑U → IsUpperSet ↑V → U ⊂ V → height U < height V) (hbound : height Finset.univ ≤ Fintype.card T) (U : Finset T) (hU : IsUpperSet ↑U) : height U = U.card

If the total height bound is the size of the poset, every upper set has height equal to its cardinality.