transversal_nonempty — Mathlib

English

The induction scheme for PushoutI φ is compatible with the monoid operations, ensuring the property persists under product.

Русский

Индукционная схема для PushoutI φ совместима с операциями моноида и сохраняет свойство под произведением.

LaTeX

$$$motives\; compatible\; with\; product$$$

Lean4

theorem transversal_nonempty (hφ : ∀ i, Injective (φ i)) : Nonempty (Transversal φ) :=
  by
  choose t ht using fun i => (φ i).range.exists_isComplement_right 1
  apply Nonempty.intro
  exact
    { injective := hφ
      set := t
      one_mem := fun i => (ht i).2
      compl := fun i => (ht i).1 }

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