nonempty — Mathlib

English

There exists a transversal pair (t, ht) with head t that provides a choice of representatives in the normal word construction.

Русский

Существует попарное транспервисное множество (t, ht) с головой t, задающее выбор представителей в конструировании нормального слова.

LaTeX

$$Nonempty (TransversalPair G A B)$$

Lean4

instance nonempty : Nonempty (TransversalPair G A B) :=
  by
  choose t ht using fun u ↦ (toSubgroup A B u).exists_isComplement_right 1
  exact ⟨⟨t, fun i ↦ (ht i).1⟩⟩

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