Documentation

LeanCamCombi.StableCombi.Formula

source
def FirstOrder.Language.Formula.IsOrderPropWith {L : Language} (n : ℕ) (M : Type u_1) [L.Structure M] (φ : L.Formula (Fin 2)) :
Prop
Equations
Instances For
    source
    def FirstOrder.Language.Formula.IsOrderProp {L : Language} (M : Type u_1) [L.Structure M] (φ : L.Formula (Fin 2)) :
    Prop
    Equations
    Instances For
      source
      def FirstOrder.Language.Formula.IsStableWith {L : Language} (n : ℕ) (M : Type u_1) [L.Structure M] (φ : L.Formula (Fin 2)) :
      Prop
      Equations
      Instances For
        source
        def FirstOrder.Language.Formula.IsStable {L : Language} (M : Type u_1) [L.Structure M] (φ : L.Formula (Fin 2)) :
        Prop
        Equations
        Instances For
          source
          def FirstOrder.Language.Formula.IsTreeBoundedWith {L : Language} (n : ℕ) (M : Type u_1) [L.Structure M] (φ : L.Formula (Fin 2)) :
          Prop
          Equations
          Instances For
            source
            @[simp]
            theorem FirstOrder.Language.Formula.not_isStableWith {L : Language} {n : ℕ} {M : Type u_1} [L.Structure M] {φ : L.Formula (Fin 2)} :
            ¬IsStableWith n M φ ↔ IsOrderPropWith n M φ
            source
            @[simp]
            theorem FirstOrder.Language.Formula.not_isOrderPropWith {L : Language} {n : ℕ} {M : Type u_1} [L.Structure M] {φ : L.Formula (Fin 2)} :
            ¬IsOrderPropWith n M φ ↔ IsStableWith n M φ
            source
            @[simp]
            theorem FirstOrder.Language.Formula.not_isStable {L : Language} {M : Type u_1} [L.Structure M] {φ : L.Formula (Fin 2)} :
            ¬IsStable M φ ↔ IsOrderProp M φ
            source
            @[simp]
            theorem FirstOrder.Language.Formula.not_isOrderProp {L : Language} {M : Type u_1} [L.Structure M] {φ : L.Formula (Fin 2)} :
            ¬IsOrderProp M φ ↔ IsStable M φ
            source
            theorem FirstOrder.Language.Formula.IsStableWith.isTreeBoundedWith {L : Language} {n : ℕ} {M : Type u_1} [L.Structure M] {φ : L.Formula (Fin 2)} (hr : IsStableWith n M φ) :
            IsTreeBoundedWith (2 ^ n + 1) M φ
            source
            theorem FirstOrder.Language.Formula.IsTreeBoundedWith.isStableWith {L : Language} {n : ℕ} {M : Type u_1} [L.Structure M] {φ : L.Formula (Fin 2)} (hr : IsTreeBoundedWith n M φ) :
            IsStableWith (2 ^ n) M φ
            source
            def FirstOrder.Language.Theory.IsOrderProp {L : Language} (T : L.Theory) :
            Prop
            Equations
            Instances For
              source
              def FirstOrder.Language.Theory.IsStable {L : Language} (T : L.Theory) :
              Prop
              Equations
              Instances For
                source
                @[simp]
                theorem FirstOrder.Language.Theory.not_isStable {L : Language} {T : L.Theory} :
                ¬T.IsStable ↔ T.IsOrderProp
                source
                @[simp]
                theorem FirstOrder.Language.Theory.not_isOrderProp {L : Language} {T : L.Theory} :
                ¬T.IsOrderProp ↔ T.IsStable