isComplement_singleton_left — Mathlib

English

IsComplement' {g} S is equivalent to S = univ.

Русский

IsComplement' {g} S эквивалентно S = univ.

LaTeX

$$$ \text{IsComplement' }\{g\} S \iff S = \mathrm{univ}. $$$

Lean4

@[to_additive]
theorem isComplement_singleton_left {g : G} : IsComplement { g } S ↔ S = univ :=
  by
  refine ⟨fun h => top_le_iff.mp fun x _ => ?_, fun h => (congr_arg _ h).mpr isComplement_singleton_univ⟩
  obtain ⟨⟨⟨z, rfl : z = g⟩, y, _⟩, hy⟩ := h.2 (g * x)
  rwa [← mul_left_cancel hy]

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