div_mem — Mathlib

English

For any P: G → Prop, ∃x ∈ H with P x⁻¹ iff ∃x ∈ H with P x.

Русский

Для любого P: G → Prop существует x ∈ H с P(x⁻¹) тогда и только тогда, есть x ∈ H с P(x).

LaTeX

$$∃ x ∈ H, P(x^{-1}) \iff ∃ x ∈ H, P(x)$$

Lean4

/-- A subgroup is closed under division. -/
@[to_additive (attr := aesop 90% (rule_sets := [SetLike])) /-- An additive subgroup is closed under subtraction. -/
    ]
theorem div_mem {x y : M} (hx : x ∈ H) (hy : y ∈ H) : x / y ∈ H := by rw [div_eq_mul_inv]; exact mul_mem hx (inv_mem hy)

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