Commit 2024-01-08 13:15 3d1cf78f

View on Github →

chore(*): use ∃ x ∈ s, p x instead of ∃ x (_ : x ∈ s), p x (#9326) This is a follow-up to #9215. It changes the following theorems and definitions:

  • IsOpen.exists_subset_affineIndependent_span_eq_top
  • IsConformalMap
  • SimpleGraph.induce_connected_of_patches
  • Submonoid.exists_list_of_mem_closure
  • AddSubmonoid.exists_list_of_mem_closure
  • AffineSubspace.mem_affineSpan_insert_iff
  • AffineBasis.exists_affine_subbasis
  • exists_affineIndependent
  • LinearMap.mem_submoduleImage
  • Basis.basis_singleton_iff
  • atom_iff_nonzero_span
  • finrank_eq_one_iff'
  • Submodule.basis_of_pid_aux
  • exists_linearIndependent_extension
  • exists_linearIndependent
  • countable_cover_nhdsWithin_of_sigma_compact
  • mem_residual Also deprecate ENNReal.exists_ne_top'.

Estimated changes

modified theorem ENNReal.exists_ne_top
modified theorem finrank_eq_one_iff'
modified theorem mem_residual