def ConNF.SupportOrbit [ConNF.Params] (β : ConNF.Λ) [ConNF.ModelData ↑β] : Type u

Equations

• ConNF.SupportOrbit β = MulAction.orbitRel.Quotient (ConNF.Allowable ↑β) (ConNF.Support ↑β)

def ConNF.SupportOrbit.mk [ConNF.Params] {β : ConNF.Λ} [ConNF.ModelData ↑β] (S : ConNF.Support ↑β) : ConNF.SupportOrbit β

The orbit of a given ordered support.

Equations

• ConNF.SupportOrbit.mk S = ⟦S⟧

theorem ConNF.SupportOrbit.eq [ConNF.Params] {β : ConNF.Λ} [ConNF.ModelData ↑β] {S : ConNF.Support ↑β} {T : ConNF.Support ↑β} : ConNF.SupportOrbit.mk S = ConNF.SupportOrbit.mk T ↔ S ∈ MulAction.orbit (ConNF.Allowable ↑β) T

instance ConNF.SupportOrbit.instSetLikeSupportSomeΛ [ConNF.Params] {β : ConNF.Λ} [ConNF.ModelData ↑β] : SetLike (ConNF.SupportOrbit β) (ConNF.Support ↑β)

Equations

• ConNF.SupportOrbit.instSetLikeSupportSomeΛ = { coe := fun (o : ConNF.SupportOrbit β) => {S : ConNF.Support ↑β | ConNF.SupportOrbit.mk S = o}, coe_injective' := ⋯ }

theorem ConNF.SupportOrbit.mem_mk [ConNF.Params] {β : ConNF.Λ} [ConNF.ModelData ↑β] (S : ConNF.Support ↑β) : S ∈ ConNF.SupportOrbit.mk S

theorem ConNF.SupportOrbit.mem_def [ConNF.Params] {β : ConNF.Λ} [ConNF.ModelData ↑β] (S : ConNF.Support ↑β) (o : ConNF.SupportOrbit β) : S ∈ o ↔ ConNF.SupportOrbit.mk S = o

@[simp]

theorem ConNF.SupportOrbit.mem_mk_iff [ConNF.Params] {β : ConNF.Λ} [ConNF.ModelData ↑β] (S : ConNF.Support ↑β) (T : ConNF.Support ↑β) : S ∈ ConNF.SupportOrbit.mk T ↔ S ∈ MulAction.orbit (ConNF.Allowable ↑β) T

theorem ConNF.SupportOrbit.smul_mem_of_mem [ConNF.Params] {β : ConNF.Λ} [ConNF.ModelData ↑β] {S : ConNF.Support ↑β} {o : ConNF.SupportOrbit β} (ρ : ConNF.Allowable ↑β) (h : S ∈ o) : ρ • S ∈ o

theorem ConNF.SupportOrbit.smul_mem_iff_mem [ConNF.Params] {β : ConNF.Λ} [ConNF.ModelData ↑β] {S : ConNF.Support ↑β} {o : ConNF.SupportOrbit β} (ρ : ConNF.Allowable ↑β) : ρ • S ∈ o ↔ S ∈ o

theorem ConNF.SupportOrbit.eq_of_mem_orbit [ConNF.Params] {β : ConNF.Λ} [ConNF.ModelData ↑β] {o₁ : ConNF.SupportOrbit β} {o₂ : ConNF.SupportOrbit β} {S₁ : ConNF.Support ↑β} {S₂ : ConNF.Support ↑β} (h₁ : S₁ ∈ o₁) (h₂ : S₂ ∈ o₂) (h : S₁ ∈ MulAction.orbit (ConNF.Allowable ↑β) S₂) : o₁ = o₂

theorem ConNF.SupportOrbit.inductionOn [ConNF.Params] {β : ConNF.Λ} [ConNF.ModelData ↑β] {motive : ConNF.SupportOrbit β → Prop} (o : ConNF.SupportOrbit β) (h : ∀ (S : ConNF.Support ↑β), motive (ConNF.SupportOrbit.mk S)) : motive o

theorem ConNF.SupportOrbit.nonempty [ConNF.Params] {β : ConNF.Λ} [ConNF.ModelData ↑β] (o : ConNF.SupportOrbit β) : {S : ConNF.Support ↑β | S ∈ o}.Nonempty

noncomputable def ConNF.SupportOrbit.out [ConNF.Params] {β : ConNF.Λ} [ConNF.ModelData ↑β] (o : ConNF.SupportOrbit β) : ConNF.Support ↑β

Equations

• o.out = Quotient.out o

theorem ConNF.SupportOrbit.out_mem [ConNF.Params] {β : ConNF.Λ} [ConNF.ModelData ↑β] (o : ConNF.SupportOrbit β) : o.out ∈ o

theorem ConNF.SupportOrbit.eq_mk_of_mem [ConNF.Params] {β : ConNF.Λ} [ConNF.ModelData ↑β] {S : ConNF.Support ↑β} {o : ConNF.SupportOrbit β} (h : S ∈ o) : o = ConNF.SupportOrbit.mk S

def ConNF.SupportOrbit.Strong [ConNF.Params] [ConNF.BasePositions] [ConNF.Level] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] (o : ConNF.SupportOrbit β) : Prop

An orbit of ordered supports is strong if it contains a strong support.

Equations

• o.Strong = ∀ S ∈ o, S.Strong