theorem lowerSemicontinuous_compactRightInfimum_and_exists_isMinOn {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace Y] [Nonempty Y] {φ : X × Y → EReal} (hφ : LowerSemicontinuous φ) : (LowerSemicontinuous fun (x : X) => sInf (Set.range fun (y : Y) => φ (x, y))) ∧ ∀ (x : X), ∃ (y : Y), IsMinOn (fun (y' : Y) => φ (x, y')) Set.univ y

Lemma 1.30: over a nonempty compact second factor, the infimum of a lower semicontinuous extended-real-valued function over the second variable is lower semicontinuous, and each fiber section attains its minimum.