finite_coe_iff

Mathlib.Data.Finite.Defs

URI: https://scilib.ai/kg/mathlib#Set.finite_coe_iff

English

Finite s is equivalent to s.Finite (coercion equivalence).

Русский

Конечность множества эквивалентна конечности его подвода через коэцию.

LaTeX

$$$\\text{finite\_coe\_iff }\\{s:\\text{Set }\\alpha\\} : \\text{Finite}(s) \\leftrightarrow s.Finite$$$

Lean4

theorem finite_coe_iff {s : Set α} : Finite s ↔ s.Finite :=
  .rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru