monovary — Mathlib

English

If ι is a Subsingleton, then for any f: ι → α and g: ι → β, Monovary f g holds.

Русский

Если ι является подмножеством одного элемента, то для любых f: ι → α и g: ι → β выполняется Monovary f g.

LaTeX

$$$[\\text{Subsingleton }\\iota]\\; \\forall f:\\iota\\to\\alpha,\\; \\forall g:\\iota\\to\\beta,\\; \\operatorname{Monovary}(f,g)$$$

Lean4

protected theorem monovary [Subsingleton ι] (f : ι → α) (g : ι → β) : Monovary f g := fun _ _ h =>
  (ne_of_apply_ne _ h.ne <| Subsingleton.elim _ _).elim

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