compl_mul_closure_one_eq_iff — Mathlib

English

t^c · closure({1}) = t^c if and only if t · closure({1}) = t.

Русский

t^c · closure({1}) = t^c тогда и только тогда, когда t · closure({1}) = t.

LaTeX

$$$t^{c} \\cdot \\overline{\\{1\\}} = t^{c} \\iff t \\cdot \\overline{\\{1\\}} = t$$$

Lean4

@[to_additive]
theorem compl_mul_closure_one_eq_iff {t : Set G} :
    tᶜ * (closure { 1 } : Set G) = tᶜ ↔ t * (closure { 1 } : Set G) = t :=
  ⟨fun h ↦ by simpa using compl_mul_closure_one_eq h, fun h ↦ compl_mul_closure_one_eq h⟩

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