isComplement_singleton_right — Mathlib

English

IsComplement S {g} iff S = univ.

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem isComplement_singleton_right {g : G} : IsComplement S { g } ↔ S = univ :=
  by
  refine ⟨fun h => top_le_iff.mp fun x _ => ?_, fun h => h ▸ isComplement_univ_singleton⟩
  obtain ⟨y, hy⟩ := h.2 (x * g)
  conv_rhs at hy => rw [← show y.2.1 = g from y.2.2]
  rw [← mul_right_cancel hy]
  exact y.1.2

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