small_neg — Mathlib

English

If a type α carries an involutive negation and S is a small set in α, then its negation −S is also a small set.

Русский

Если тип α имеет инволютивное отрицание и S — маленькое множество в α, то и −S тоже маленькое множество.

LaTeX

$$$ \\text{Small}(-S) $$$

Lean4

instance small_neg [InvolutiveNeg α] [Small.{u} s] : Small.{u} (-s :) :=
  by
  rw [← Set.image_neg_eq_neg]
  infer_instance

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