range_inl

Mathlib.Data.Set.Image

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

English

The range of Sum.inl is the set of all elements of the form (x, Bool.true) where Sum.isLeft holds.

Русский

Диапазон Sum.inl состоит из элементов вида (x, Bool.true) при условии Sum.isLeft.

LaTeX

$$$ \\mathrm{range}(\\mathrm{Sum.inl}) = \\{ x \\mid \\mathrm{Sum.isLeft}\,x \\}$. $$

Lean4

theorem range_inl : range (@Sum.inl α β) = {x | Sum.isLeft x} := by ext (_ | _) <;> simp

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

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

Разделы

Аффилиация

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