exists_inv_mem_iff_exists_mem — Mathlib

English

There exists x ∈ K with x ∈ K and P x^{-1} if and only if there exists x ∈ K with P x.

Русский

Существует x ∈ K с x ∈ K и P(x^{-1}) тогда и только тогда существует x ∈ K с P(x).

LaTeX

$$$\\exists x \\in K, P(x^{-1}) \\iff \\exists x \\in K, P(x)$$$

Lean4

@[to_additive]
protected theorem exists_inv_mem_iff_exists_mem (K : Subgroup G) {P : G → Prop} :
    (∃ x : G, x ∈ K ∧ P x⁻¹) ↔ ∃ x ∈ K, P x :=
  exists_inv_mem_iff_exists_mem

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