Commit 2023-12-26 16:00 be0b59d2

View on Github →

chore(*): use ∀ s ⊆ t, _ etc (#9276) Changes in this PR shouldn't change the public API. The only changes about ∃ x ∈ s, _ is inside a proof.

Estimated changes

modified theorem Finset.card_mul_pow_le
modified theorem Nat.prime_def_lt''
modified theorem lowerSemicontinuousAt_biSup
modified theorem lowerSemicontinuousOn_biSup
modified theorem lowerSemicontinuous_biSup
modified theorem upperSemicontinuousAt_biInf
modified theorem upperSemicontinuousOn_biInf
modified theorem upperSemicontinuous_biInf