Upper-set lines remember their supports

theorem MagnitudeConjecture.PosetSpace.line_support_subset_of_nonzero {k T : Type u} [Field k] [PartialOrder T] {U V : Set T} {hU : IsUpperSet U} {hV : IsUpperSet V} (f : line k T U hU ⟶ line k T V hV) (hf : f ≠ 0) : U ⊆ V

A nonzero map between upper-set lines forces inclusion of their supports.

theorem MagnitudeConjecture.PosetSpace.lineIso_hom_ne_zero {k T : Type u} [Field k] [PartialOrder T] {U V : Set T} {hU : IsUpperSet U} {hV : IsUpperSet V} (e : line k T U hU ≅ line k T V hV) : e.hom ≠ 0

The hom of an isomorphism between upper-set lines is nonzero.

theorem MagnitudeConjecture.PosetSpace.line_support_eq_of_iso {k T : Type u} [Field k] [PartialOrder T] {U V : Set T} {hU : IsUpperSet U} {hV : IsUpperSet V} (e : line k T U hU ≅ line k T V hV) : U = V

Isomorphic upper-set lines have equal supports.