Commit 2022-02-10 10:46 f32fda7c

feat(set_theory/ordinal_arithmetic): More lsub and blsub lemmas (#11848) We prove variants of sup_typein, which serve as analogs for blsub_id. We also prove sup_eq_lsub_or_sup_succ_eq_lsub, which combines sup_le_lsub and lsub_le_sup_succ.