monovaryOn — Mathlib

English

If ι is Subsingleton, then for any f: ι → α, g: ι → β, and s ⊆ ι, MonovaryOn f g s holds.

Русский

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

LaTeX

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

Lean4

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

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