take_self_eq_iff

Mathlib.Data.List.TakeDrop

URI: https://scilib.ai/kg/mathlib#List.take_self_eq_iff

English

The equivalence is the same as take_eq_self_iff but with reversed commutativity: x = x.take n iff x.length ≤ n.

Русский

Эквивалентность эквивалентна take_eq_self_iff, но с перестановкой: x = x.take n ↔ x.length ≤ n.

LaTeX

$$$ x = x.take n \iff x.length \le n $$$

Lean4

@[simp]
theorem take_self_eq_iff (x : List α) {n : ℕ} : x = x.take n ↔ x.length ≤ n := by rw [Eq.comm, take_eq_self_iff]

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

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

Разделы

Аффилиация

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