lookmap #
@[simp]
theorem
List.lookmap_cons_none
{α : Type u_1}
(f : α → Option α)
{a : α}
(l : List α)
(h : f a = none)
:
lookmap f (a :: l) = a :: lookmap f l
@[simp]
theorem
List.lookmap_cons_some
{α : Type u_1}
(f : α → Option α)
{a b : α}
(l : List α)
(h : f a = some b)
:
lookmap f (a :: l) = b :: l
theorem
List.lookmap_cons
{α : Type u_1}
(f : α → Option α)
{a : α}
{l : List α}
:
lookmap f (a :: l) = match f a with
| none => a :: lookmap f l
| some b => b :: l
theorem
List.lookmap_congr
{α : Type u_1}
{f g : α → Option α}
{l : List α}
:
(∀ a ∈ l, f a = g a) → lookmap f l = lookmap g l
theorem
List.lookmap_of_forall_not
{α : Type u_1}
(f : α → Option α)
{l : List α}
(H : ∀ a ∈ l, f a = none)
:
lookmap f l = l
theorem
List.lookmap_map_eq
{α : Type u_1}
{β : Type u_2}
(f : α → Option α)
(g : α → β)
(h : ∀ (a b : α), b ∈ f a → g a = g b)
(l : List α)
:
map g (lookmap f l) = map g l
theorem
List.lookmap_id'
{α : Type u_1}
(f : α → Option α)
(h : ∀ (a b : α), b ∈ f a → a = b)
(l : List α)
:
lookmap f l = l
@[simp]
theorem
List.length_lookmap
{α : Type u_1}
(f : α → Option α)
(l : List α)
:
(lookmap f l).length = l.length
theorem
List.perm_lookmap
{α : Type u_1}
(f : α → Option α)
{l₁ l₂ : List α}
(H : Pairwise (fun (a b : α) => ∀ c ∈ f a, ∀ d ∈ f b, a = b ∧ c = d) l₁)
(p : l₁.Perm l₂)
:
(lookmap f l₁).Perm (lookmap f l₂)