Equations
- ConNF.instFOAAssumptions = ConNF.MainInduction.FOA.foaAssumptions
Instances For
theorem
ConNF.symmetric_of_image_singleton_symmetric'
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
[iγ : ConNF.LtLevel ↑γ]
(hγ : ↑γ < ↑β)
(s : Set (ConNF.TSet ↑γ))
(h : ConNF.Symmetric ⋯ (ConNF.ModelData.TSet.singleton ⋯ '' s))
:
ConNF.Symmetric ⋯ s
theorem
ConNF.symmetric_of_image_singleton_symmetric
[ConNF.Params]
{α : ConNF.Λ}
{β : ConNF.Λ}
{γ : ConNF.Λ}
(hβ : β < α)
(hγ : γ < β)
(s : Set (ConNF.TSet ↑γ))
(h : ConNF.Symmetric hβ (ConNF.ModelData.TSet.singleton hγ '' s))
:
ConNF.Symmetric hγ s