Documentation

NominalSets.Option

Optional Types #

This file formalizes definitions and results about permutations and supports for Option types.

Permutations #

instance NominalSets.Option.instPermActionOption {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] :

PermAction 𝔸 (Option X)

Equations

NominalSets.Option.instPermActionOption = { perm := fun (π : NominalSets.Perm 𝔸) => Option.map (NominalSets.perm π), perm_one := ⋯, perm_mul := ⋯ }

theorem NominalSets.Option.perm_def {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] (π : Perm 𝔸) (a✝ : Option X) :

perm π a✝ = Option.map (perm π) a✝

@[simp]

theorem NominalSets.Option.perm_none {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] (π : Perm 𝔸) :

perm π none = none

@[simp]

theorem NominalSets.Option.perm_some {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] (π : Perm 𝔸) (x : X) :

perm π (some x) = some (perm π x)

@[simp]

theorem NominalSets.Option.perm_elim {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] (π : Perm 𝔸) (z : Y) (f : X → Y) (x : Option X) :

perm π (x.elim z f) = (perm π x).elim (perm π z) (perm π f)

instance NominalSets.Option.instDiscretePermActionOption {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] [DiscretePermAction 𝔸 X] :

DiscretePermAction 𝔸 (Option X)

Supports #

@[simp]

theorem NominalSets.Option.isSupportOf_none {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] (A : Finset 𝔸) :

IsSupportOf A none

@[simp]

theorem NominalSets.Option.isSupportOf_some {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] (A : Finset 𝔸) (x : X) :

IsSupportOf A (some x) ↔ IsSupportOf A x

@[simp]

theorem NominalSets.Option.isSupported_none {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] :

IsSupported 𝔸 none

@[simp]

theorem NominalSets.Option.isSupported_some {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] (x : X) :

IsSupported 𝔸 (some x) ↔ IsSupported 𝔸 x

instance NominalSets.Option.instNominalOption {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] [Nominal 𝔸 X] :

Nominal 𝔸 (Option X)

@[simp]

theorem NominalSets.Option.supp_none {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] [Nominal 𝔸 X] :

supp 𝔸 none = ∅

@[simp]

theorem NominalSets.Option.supp_some {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] [Nominal 𝔸 X] (x : X) :

supp 𝔸 (some x) = supp 𝔸 x

@[simp]

theorem NominalSets.Option.isSupportedF_none {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] :

IsSupportedF 𝔸 fun (x : X) => none

@[simp]

theorem NominalSets.Option.isSupportedF_some {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] :

IsSupportedF 𝔸 some

theorem NominalSets.Option.isSupportedF_elim {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [PermAction 𝔸 X] [PermAction 𝔸 Y] [PermAction 𝔸 Z] {f : X → Option Y} (hf : IsSupportedF 𝔸 f) {g : X → Z} (hg : IsSupportedF 𝔸 g) {h : X → Y → Z} (hh : IsSupportedF 𝔸 fun (x : X × Y) => match x with | (x, y) => h x y) :

IsSupportedF 𝔸 fun (x : X) => (f x).elim (g x) (h x)

Equivariance #

@[simp]

theorem NominalSets.Option.equivariant_none {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] :

Equivariant 𝔸 fun (x : X) => none

@[simp]

theorem NominalSets.Option.equivariant_some {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] :

Equivariant 𝔸 some

theorem NominalSets.Option.equivariant_elim {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [PermAction 𝔸 X] [PermAction 𝔸 Y] [PermAction 𝔸 Z] {f : X → Option Y} (hf : Equivariant 𝔸 f) {g : X → Z} (hg : Equivariant 𝔸 g) {h : X → Y → Z} (hh : Equivariant 𝔸 fun (x : X × Y) => match x with | (x, y) => h x y) :

Equivariant 𝔸 fun (x : X) => (f x).elim (g x) (h x)