exists_mk — Mathlib

English

There exists a representative in α for every quotient element in α / s: (∃ x : α / s, C x) ↔ ∃ x : α, C x.

Русский

Существует представитель в α для каждого элемента в α / s: (∃ x : α / s, C x) ⇔ ∃ x : α, C x.

LaTeX

$${C : HasQuotient.Quotient α s → Prop} : (∃ x : α / s, C x) ↔ ∃ x : α, C x$$

Lean4

@[to_additive]
theorem exists_mk {C : α ⧸ s → Prop} : (∃ x : α ⧸ s, C x) ↔ ∃ x : α, C x :=
  mk_surjective.exists

Похожие утверждения