ObjectProperty is a complete lattice

@[simp]

theorem CategoryTheory.ObjectProperty.prop_inf_iff {C : Type u} [Category.{v, u} C] (P Q : ObjectProperty C) (X : C) : (P ⊓ Q) X ↔ P X ∧ Q X

@[simp]

theorem CategoryTheory.ObjectProperty.prop_sup_iff {C : Type u} [Category.{v, u} C] (P Q : ObjectProperty C) (X : C) : (P ⊔ Q) X ↔ P X ∨ Q X

instance CategoryTheory.ObjectProperty.nonempty_sup_left {C : Type u} [Category.{v, u} C] (P Q : ObjectProperty C) [P.Nonempty] : (P ⊔ Q).Nonempty

instance CategoryTheory.ObjectProperty.nonempty_sup_right {C : Type u} [Category.{v, u} C] (P Q : ObjectProperty C) [Q.Nonempty] : (P ⊔ Q).Nonempty

instance CategoryTheory.ObjectProperty.nonempty_top {C : Type u} [Category.{v, u} C] [Nonempty C] : ⊤.Nonempty

theorem CategoryTheory.ObjectProperty.isoClosure_sup {C : Type u} [Category.{v, u} C] (P Q : ObjectProperty C) : (P ⊔ Q).isoClosure = P.isoClosure ⊔ Q.isoClosure

instance CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsMax {C : Type u} [Category.{v, u} C] (P Q : ObjectProperty C) [P.IsClosedUnderIsomorphisms] [Q.IsClosedUnderIsomorphisms] : (P ⊔ Q).IsClosedUnderIsomorphisms

instance CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsMin {C : Type u} [Category.{v, u} C] (P Q : ObjectProperty C) [P.IsClosedUnderIsomorphisms] [Q.IsClosedUnderIsomorphisms] : (P ⊓ Q).IsClosedUnderIsomorphisms

instance CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsBot {C : Type u} [Category.{v, u} C] : ⊥.IsClosedUnderIsomorphisms

instance CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsTop {C : Type u} [Category.{v, u} C] : ⊤.IsClosedUnderIsomorphisms

@[simp]

theorem CategoryTheory.ObjectProperty.prop_iSup_iff {C : Type u} [Category.{v, u} C] {α : Sort u_1} (P : α → ObjectProperty C) (X : C) : (⨆ (a : α), P a) X ↔ ∃ (a : α), P a X

theorem CategoryTheory.ObjectProperty.nonempty_iSup {C : Type u} [Category.{v, u} C] {α : Sort u_1} (P : α → ObjectProperty C) (a : α) [(P a).Nonempty] : (⨆ (a : α), P a).Nonempty

theorem CategoryTheory.ObjectProperty.isoClosure_iSup {C : Type u} [Category.{v, u} C] {α : Sort u_1} (P : α → ObjectProperty C) : (⨆ (a : α), P a).isoClosure = ⨆ (a : α), (P a).isoClosure

instance CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsISup {C : Type u} [Category.{v, u} C] {α : Sort u_1} (P : α → ObjectProperty C) [∀ (a : α), (P a).IsClosedUnderIsomorphisms] : (⨆ (a : α), P a).IsClosedUnderIsomorphisms

instance CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsIInf {C : Type u} [Category.{v, u} C] {α : Sort u_1} (P : α → ObjectProperty C) [∀ (a : α), (P a).IsClosedUnderIsomorphisms] : (⨅ (a : α), P a).IsClosedUnderIsomorphisms

theorem CategoryTheory.ObjectProperty.ne_bot_iff_exists {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) : ¬P = ⊥ ↔ ∃ (X : C), P X

theorem CategoryTheory.ObjectProperty.nonempty_iff_ne_bot {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) : P.Nonempty ↔ ¬P = ⊥

theorem CategoryTheory.ObjectProperty.not_nonempty_iff_eq_bot {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) : ¬P.Nonempty ↔ P = ⊥

@[simp]

theorem CategoryTheory.ObjectProperty.ι_map_top {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) : ⊤.map P.ι = P.isoClosure