antivaryOn — Mathlib

English

If ι is Subsingleton, then for any f: ι → α and g: ι → β, and s ∈ Set ι, AntivaryOn f g s holds.

Русский

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

LaTeX

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

Lean4

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

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