compl_image_coe — Mathlib

English

Let X be a type and i: X → OnePoint X be the canonical inclusion. For any subset S ⊆ X, the complement in OnePoint X of the image i[S] is exactly the image of the complement of S, together with the infinity point. In symbols: ((i''S))^c = i''(S^c) ∪ {∞}.

Русский

Пусть X — множество, i: X → OnePoint X — каноническое вложение. Для любой подмножества S ⊆ X комплемент образа i[S] в OnePoint X равен образу дополнения S вместе с точкой бесконечности: ((i''S))^c = i''(S^c) ∪ {∞}.

LaTeX

$$$((\\iota)'' S)^c = (\\iota)'' S^c \\cup \\{\\infty\\}.$$$

Lean4

theorem compl_image_coe (s : Set X) : ((↑) '' s : Set (OnePoint X))ᶜ = (↑) '' sᶜ ∪ {∞} := by
  rw [coe_injective.compl_image_eq, compl_range_coe]

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