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

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.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

@[simp]

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