order.disjoint - mathlib3 docs

def disjoint {α : Type u_1} [partial_order α] [order_bot α] (a b : α) :

Prop

Two elements of a lattice are disjoint if their inf is the bottom element. (This generalizes disjoint sets, viewed as members of the subset lattice.)

Note that we define this without reference to ⊓, as this allows us to talk about orders where the infimum is not unique, or where implementing has_inf would require additional decidable arguments.

Equations

disjoint a b = ∀ ⦃x : α⦄, x ≤ a → x ≤ b → x ≤ ⊥

Instances for disjoint

finset.decidable_disjoint

source

theorem disjoint.comm {α : Type u_1} [partial_order α] [order_bot α] {a b : α} :

disjoint a b ↔ disjoint b a

source

@[symm]

theorem disjoint.symm {α : Type u_1} [partial_order α] [order_bot α] ⦃a b : α⦄ :

disjoint a b → disjoint b a

source

theorem symmetric_disjoint {α : Type u_1} [partial_order α] [order_bot α] :

symmetric disjoint

source

@[simp]

theorem disjoint_bot_left {α : Type u_1} [partial_order α] [order_bot α] {a : α} :

disjoint ⊥ a

source

@[simp]

theorem disjoint_bot_right {α : Type u_1} [partial_order α] [order_bot α] {a : α} :

disjoint a ⊥

source

theorem disjoint.mono {α : Type u_1} [partial_order α] [order_bot α] {a b c d : α} (h₁ : a ≤ b) (h₂ : c ≤ d) :

disjoint b d → disjoint a c

source

theorem disjoint.mono_left {α : Type u_1} [partial_order α] [order_bot α] {a b c : α} (h : a ≤ b) :

disjoint b c → disjoint a c

source

theorem disjoint.mono_right {α : Type u_1} [partial_order α] [order_bot α] {a b c : α} :

b ≤ c → disjoint a c → disjoint a b

source

@[simp]

theorem disjoint_self {α : Type u_1} [partial_order α] [order_bot α] {a : α} :

disjoint a a ↔ a = ⊥

source

theorem disjoint.eq_bot_of_self {α : Type u_1} [partial_order α] [order_bot α] {a : α} :

disjoint a a → a = ⊥

Alias of the forward direction of disjoint_self.

source

theorem disjoint.ne {α : Type u_1} [partial_order α] [order_bot α] {a b : α} (ha : a ≠ ⊥) (hab : disjoint a b) :

a ≠ b

source

theorem disjoint.eq_bot_of_le {α : Type u_1} [partial_order α] [order_bot α] {a b : α} (hab : disjoint a b) (h : a ≤ b) :

a = ⊥

source

theorem disjoint.eq_bot_of_ge {α : Type u_1} [partial_order α] [order_bot α] {a b : α} (hab : disjoint a b) :

b ≤ a → b = ⊥

source

@[simp]

theorem disjoint_top {α : Type u_1} [partial_order α] [bounded_order α] {a : α} :

disjoint a ⊤ ↔ a = ⊥

source

@[simp]

theorem top_disjoint {α : Type u_1} [partial_order α] [bounded_order α] {a : α} :

disjoint ⊤ a ↔ a = ⊥

source

theorem disjoint_iff_inf_le {α : Type u_1} [semilattice_inf α] [order_bot α] {a b : α} :

disjoint a b ↔ a ⊓ b ≤ ⊥

source

theorem disjoint_iff {α : Type u_1} [semilattice_inf α] [order_bot α] {a b : α} :

disjoint a b ↔ a ⊓ b = ⊥

source

theorem disjoint.le_bot {α : Type u_1} [semilattice_inf α] [order_bot α] {a b : α} :

disjoint a b → a ⊓ b ≤ ⊥

source

theorem disjoint.eq_bot {α : Type u_1} [semilattice_inf α] [order_bot α] {a b : α} :

disjoint a b → a ⊓ b = ⊥

source

theorem disjoint_assoc {α : Type u_1} [semilattice_inf α] [order_bot α] {a b c : α} :

disjoint (a ⊓ b) c ↔ disjoint a (b ⊓ c)

source

theorem disjoint_left_comm {α : Type u_1} [semilattice_inf α] [order_bot α] {a b c : α} :

disjoint a (b ⊓ c) ↔ disjoint b (a ⊓ c)

source

theorem disjoint_right_comm {α : Type u_1} [semilattice_inf α] [order_bot α] {a b c : α} :

disjoint (a ⊓ b) c ↔ disjoint (a ⊓ c) b

source

theorem disjoint.inf_left {α : Type u_1} [semilattice_inf α] [order_bot α] {a b : α} (c : α) (h : disjoint a b) :

disjoint (a ⊓ c) b

source

theorem disjoint.inf_left' {α : Type u_1} [semilattice_inf α] [order_bot α] {a b : α} (c : α) (h : disjoint a b) :

disjoint (c ⊓ a) b

source

theorem disjoint.inf_right {α : Type u_1} [semilattice_inf α] [order_bot α] {a b : α} (c : α) (h : disjoint a b) :

disjoint a (b ⊓ c)

source

theorem disjoint.inf_right' {α : Type u_1} [semilattice_inf α] [order_bot α] {a b : α} (c : α) (h : disjoint a b) :

disjoint a (c ⊓ b)

source

theorem disjoint.of_disjoint_inf_of_le {α : Type u_1} [semilattice_inf α] [order_bot α] {a b c : α} (h : disjoint (a ⊓ b) c) (hle : a ≤ c) :

disjoint a b

source

theorem disjoint.of_disjoint_inf_of_le' {α : Type u_1} [semilattice_inf α] [order_bot α] {a b c : α} (h : disjoint (a ⊓ b) c) (hle : b ≤ c) :

disjoint a b

source

@[simp]

theorem disjoint_sup_left {α : Type u_1} [distrib_lattice α] [order_bot α] {a b c : α} :

disjoint (a ⊔ b) c ↔ disjoint a c ∧ disjoint b c

source

@[simp]

theorem disjoint_sup_right {α : Type u_1} [distrib_lattice α] [order_bot α] {a b c : α} :

disjoint a (b ⊔ c) ↔ disjoint a b ∧ disjoint a c

source

theorem disjoint.sup_left {α : Type u_1} [distrib_lattice α] [order_bot α] {a b c : α} (ha : disjoint a c) (hb : disjoint b c) :

disjoint (a ⊔ b) c

source

theorem disjoint.sup_right {α : Type u_1} [distrib_lattice α] [order_bot α] {a b c : α} (hb : disjoint a b) (hc : disjoint a c) :

disjoint a (b ⊔ c)

source

theorem disjoint.left_le_of_le_sup_right {α : Type u_1} [distrib_lattice α] [order_bot α] {a b c : α} (h : a ≤ b ⊔ c) (hd : disjoint a c) :

a ≤ b

source

theorem disjoint.left_le_of_le_sup_left {α : Type u_1} [distrib_lattice α] [order_bot α] {a b c : α} (h : a ≤ c ⊔ b) (hd : disjoint a c) :

a ≤ b

source

def codisjoint {α : Type u_1} [partial_order α] [order_top α] (a b : α) :

Prop

Two elements of a lattice are codisjoint if their sup is the top element.

Note that we define this without reference to ⊔, as this allows us to talk about orders where the supremum is not unique, or where implement has_sup would require additional decidable arguments.

Equations

codisjoint a b = ∀ ⦃x : α⦄, a ≤ x → b ≤ x → ⊤ ≤ x

Instances for codisjoint

finset.decidable_codisjoint

source

theorem codisjoint.comm {α : Type u_1} [partial_order α] [order_top α] {a b : α} :

codisjoint a b ↔ codisjoint b a

source

@[symm]

theorem codisjoint.symm {α : Type u_1} [partial_order α] [order_top α] ⦃a b : α⦄ :

codisjoint a b → codisjoint b a

source

theorem symmetric_codisjoint {α : Type u_1} [partial_order α] [order_top α] :

symmetric codisjoint

source

@[simp]

theorem codisjoint_top_left {α : Type u_1} [partial_order α] [order_top α] {a : α} :

codisjoint ⊤ a

source

@[simp]

theorem codisjoint_top_right {α : Type u_1} [partial_order α] [order_top α] {a : α} :

codisjoint a ⊤

source

theorem codisjoint.mono {α : Type u_1} [partial_order α] [order_top α] {a b c d : α} (h₁ : a ≤ b) (h₂ : c ≤ d) :

codisjoint a c → codisjoint b d

source

theorem codisjoint.mono_left {α : Type u_1} [partial_order α] [order_top α] {a b c : α} (h : a ≤ b) :

codisjoint a c → codisjoint b c

source

theorem codisjoint.mono_right {α : Type u_1} [partial_order α] [order_top α] {a b c : α} :

b ≤ c → codisjoint a b → codisjoint a c

source

@[simp]

theorem codisjoint_self {α : Type u_1} [partial_order α] [order_top α] {a : α} :

codisjoint a a ↔ a = ⊤

source

theorem codisjoint.eq_top_of_self {α : Type u_1} [partial_order α] [order_top α] {a : α} :

codisjoint a a → a = ⊤

Alias of the forward direction of codisjoint_self.

source

theorem codisjoint.ne {α : Type u_1} [partial_order α] [order_top α] {a b : α} (ha : a ≠ ⊤) (hab : codisjoint a b) :

a ≠ b

source

theorem codisjoint.eq_top_of_le {α : Type u_1} [partial_order α] [order_top α] {a b : α} (hab : codisjoint a b) (h : b ≤ a) :

a = ⊤

source

theorem codisjoint.eq_top_of_ge {α : Type u_1} [partial_order α] [order_top α] {a b : α} (hab : codisjoint a b) :

a ≤ b → b = ⊤

source

@[simp]

theorem codisjoint_bot {α : Type u_1} [partial_order α] [bounded_order α] {a : α} :

codisjoint a ⊥ ↔ a = ⊤

source

@[simp]

theorem bot_codisjoint {α : Type u_1} [partial_order α] [bounded_order α] {a : α} :

codisjoint ⊥ a ↔ a = ⊤

source

theorem codisjoint_iff_le_sup {α : Type u_1} [semilattice_sup α] [order_top α] {a b : α} :

codisjoint a b ↔ ⊤ ≤ a ⊔ b

source

theorem codisjoint_iff {α : Type u_1} [semilattice_sup α] [order_top α] {a b : α} :

codisjoint a b ↔ a ⊔ b = ⊤

source

theorem codisjoint.top_le {α : Type u_1} [semilattice_sup α] [order_top α] {a b : α} :

codisjoint a b → ⊤ ≤ a ⊔ b

source

theorem codisjoint.eq_top {α : Type u_1} [semilattice_sup α] [order_top α] {a b : α} :

codisjoint a b → a ⊔ b = ⊤

source

theorem codisjoint_assoc {α : Type u_1} [semilattice_sup α] [order_top α] {a b c : α} :

codisjoint (a ⊔ b) c ↔ codisjoint a (b ⊔ c)

source

theorem codisjoint_left_comm {α : Type u_1} [semilattice_sup α] [order_top α] {a b c : α} :

codisjoint a (b ⊔ c) ↔ codisjoint b (a ⊔ c)

source

theorem codisjoint_right_comm {α : Type u_1} [semilattice_sup α] [order_top α] {a b c : α} :

codisjoint (a ⊔ b) c ↔ codisjoint (a ⊔ c) b

source

theorem codisjoint.sup_left {α : Type u_1} [semilattice_sup α] [order_top α] {a b : α} (c : α) (h : codisjoint a b) :

codisjoint (a ⊔ c) b

source

theorem codisjoint.sup_left' {α : Type u_1} [semilattice_sup α] [order_top α] {a b : α} (c : α) (h : codisjoint a b) :

codisjoint (c ⊔ a) b

source

theorem codisjoint.sup_right {α : Type u_1} [semilattice_sup α] [order_top α] {a b : α} (c : α) (h : codisjoint a b) :

codisjoint a (b ⊔ c)

source

theorem codisjoint.sup_right' {α : Type u_1} [semilattice_sup α] [order_top α] {a b : α} (c : α) (h : codisjoint a b) :

codisjoint a (c ⊔ b)

source

theorem codisjoint.of_codisjoint_sup_of_le {α : Type u_1} [semilattice_sup α] [order_top α] {a b c : α} (h : codisjoint (a ⊔ b) c) (hle : c ≤ a) :

codisjoint a b

source

theorem codisjoint.of_codisjoint_sup_of_le' {α : Type u_1} [semilattice_sup α] [order_top α] {a b c : α} (h : codisjoint (a ⊔ b) c) (hle : c ≤ b) :

codisjoint a b

source

@[simp]

theorem codisjoint_inf_left {α : Type u_1} [distrib_lattice α] [order_top α] {a b c : α} :

codisjoint (a ⊓ b) c ↔ codisjoint a c ∧ codisjoint b c

source

@[simp]

theorem codisjoint_inf_right {α : Type u_1} [distrib_lattice α] [order_top α] {a b c : α} :

codisjoint a (b ⊓ c) ↔ codisjoint a b ∧ codisjoint a c

source

theorem codisjoint.inf_left {α : Type u_1} [distrib_lattice α] [order_top α] {a b c : α} (ha : codisjoint a c) (hb : codisjoint b c) :

codisjoint (a ⊓ b) c

source

theorem codisjoint.inf_right {α : Type u_1} [distrib_lattice α] [order_top α] {a b c : α} (hb : codisjoint a b) (hc : codisjoint a c) :

codisjoint a (b ⊓ c)

source

theorem codisjoint.left_le_of_le_inf_right {α : Type u_1} [distrib_lattice α] [order_top α] {a b c : α} (h : a ⊓ b ≤ c) (hd : codisjoint b c) :

a ≤ c

source

theorem codisjoint.left_le_of_le_inf_left {α : Type u_1} [distrib_lattice α] [order_top α] {a b c : α} (h : b ⊓ a ≤ c) (hd : codisjoint b c) :

a ≤ c

source

theorem disjoint.dual {α : Type u_1} [semilattice_inf α] [order_bot α] {a b : α} :

disjoint a b → codisjoint (⇑order_dual.to_dual a) (⇑order_dual.to_dual b)

source

theorem codisjoint.dual {α : Type u_1} [semilattice_sup α] [order_top α] {a b : α} :

codisjoint a b → disjoint (⇑order_dual.to_dual a) (⇑order_dual.to_dual b)

source

@[simp]

theorem disjoint_to_dual_iff {α : Type u_1} [semilattice_sup α] [order_top α] {a b : α} :

disjoint (⇑order_dual.to_dual a) (⇑order_dual.to_dual b) ↔ codisjoint a b

source

@[simp]

theorem disjoint_of_dual_iff {α : Type u_1} [semilattice_inf α] [order_bot α] {a b : αᵒᵈ} :

disjoint (⇑order_dual.of_dual a) (⇑order_dual.of_dual b) ↔ codisjoint a b

source

@[simp]

theorem codisjoint_to_dual_iff {α : Type u_1} [semilattice_inf α] [order_bot α] {a b : α} :

codisjoint (⇑order_dual.to_dual a) (⇑order_dual.to_dual b) ↔ disjoint a b

source

@[simp]

theorem codisjoint_of_dual_iff {α : Type u_1} [semilattice_sup α] [order_top α] {a b : αᵒᵈ} :

codisjoint (⇑order_dual.of_dual a) (⇑order_dual.of_dual b) ↔ disjoint a b

source

theorem disjoint.le_of_codisjoint {α : Type u_1} [distrib_lattice α] [bounded_order α] {a b c : α} (hab : disjoint a b) (hbc : codisjoint b c) :

a ≤ c

source

structure is_compl {α : Type u_1} [partial_order α] [bounded_order α] (x y : α) :

Prop

disjoint : disjoint x y
codisjoint : codisjoint x y

Two elements x and y are complements of each other if x ⊔ y = ⊤ and x ⊓ y = ⊥.

Instances for is_compl

finset.decidable_is_compl

source

theorem is_compl_iff {α : Type u_1} [partial_order α] [bounded_order α] {a b : α} :

is_compl a b ↔ disjoint a b ∧ codisjoint a b

source

@[protected, symm]

theorem is_compl.symm {α : Type u_1} [partial_order α] [bounded_order α] {x y : α} (h : is_compl x y) :

is_compl y x

source

theorem is_compl.dual {α : Type u_1} [partial_order α] [bounded_order α] {x y : α} (h : is_compl x y) :

is_compl (⇑order_dual.to_dual x) (⇑order_dual.to_dual y)

source

theorem is_compl.of_dual {α : Type u_1} [partial_order α] [bounded_order α] {a b : αᵒᵈ} (h : is_compl a b) :

is_compl (⇑order_dual.of_dual a) (⇑order_dual.of_dual b)

source

theorem is_compl.of_le {α : Type u_1} [lattice α] [bounded_order α] {x y : α} (h₁ : x ⊓ y ≤ ⊥) (h₂ : ⊤ ≤ x ⊔ y) :

is_compl x y

source

theorem is_compl.of_eq {α : Type u_1} [lattice α] [bounded_order α] {x y : α} (h₁ : x ⊓ y = ⊥) (h₂ : x ⊔ y = ⊤) :

is_compl x y

source

theorem is_compl.inf_eq_bot {α : Type u_1} [lattice α] [bounded_order α] {x y : α} (h : is_compl x y) :

x ⊓ y = ⊥

source

theorem is_compl.sup_eq_top {α : Type u_1} [lattice α] [bounded_order α] {x y : α} (h : is_compl x y) :

x ⊔ y = ⊤

source

theorem is_compl.inf_left_le_of_le_sup_right {α : Type u_1} [distrib_lattice α] [bounded_order α] {a b x y : α} (h : is_compl x y) (hle : a ≤ b ⊔ y) :

a ⊓ x ≤ b

source

theorem is_compl.le_sup_right_iff_inf_left_le {α : Type u_1} [distrib_lattice α] [bounded_order α] {x y a b : α} (h : is_compl x y) :

a ≤ b ⊔ y ↔ a ⊓ x ≤ b

source

theorem is_compl.inf_left_eq_bot_iff {α : Type u_1} [distrib_lattice α] [bounded_order α] {x y z : α} (h : is_compl y z) :

x ⊓ y = ⊥ ↔ x ≤ z

source

theorem is_compl.inf_right_eq_bot_iff {α : Type u_1} [distrib_lattice α] [bounded_order α] {x y z : α} (h : is_compl y z) :

x ⊓ z = ⊥ ↔ x ≤ y

source

theorem is_compl.disjoint_left_iff {α : Type u_1} [distrib_lattice α] [bounded_order α] {x y z : α} (h : is_compl y z) :

disjoint x y ↔ x ≤ z

source

theorem is_compl.disjoint_right_iff {α : Type u_1} [distrib_lattice α] [bounded_order α] {x y z : α} (h : is_compl y z) :

disjoint x z ↔ x ≤ y

source

theorem is_compl.le_left_iff {α : Type u_1} [distrib_lattice α] [bounded_order α] {x y z : α} (h : is_compl x y) :

z ≤ x ↔ disjoint z y

source

theorem is_compl.le_right_iff {α : Type u_1} [distrib_lattice α] [bounded_order α] {x y z : α} (h : is_compl x y) :

z ≤ y ↔ disjoint z x

source

theorem is_compl.left_le_iff {α : Type u_1} [distrib_lattice α] [bounded_order α] {x y z : α} (h : is_compl x y) :

x ≤ z ↔ codisjoint z y

source

theorem is_compl.right_le_iff {α : Type u_1} [distrib_lattice α] [bounded_order α] {x y z : α} (h : is_compl x y) :

y ≤ z ↔ codisjoint z x

source

@[protected]

theorem is_compl.antitone {α : Type u_1} [distrib_lattice α] [bounded_order α] {x y x' y' : α} (h : is_compl x y) (h' : is_compl x' y') (hx : x ≤ x') :

y' ≤ y

source

theorem is_compl.right_unique {α : Type u_1} [distrib_lattice α] [bounded_order α] {x y z : α} (hxy : is_compl x y) (hxz : is_compl x z) :

y = z

source

theorem is_compl.left_unique {α : Type u_1} [distrib_lattice α] [bounded_order α] {x y z : α} (hxz : is_compl x z) (hyz : is_compl y z) :

x = y

source

theorem is_compl.sup_inf {α : Type u_1} [distrib_lattice α] [bounded_order α] {x y x' y' : α} (h : is_compl x y) (h' : is_compl x' y') :

is_compl (x ⊔ x') (y ⊓ y')

source

theorem is_compl.inf_sup {α : Type u_1} [distrib_lattice α] [bounded_order α] {x y x' y' : α} (h : is_compl x y) (h' : is_compl x' y') :

is_compl (x ⊓ x') (y ⊔ y')

source

@[protected]

theorem prod.disjoint_iff {α : Type u_1} {β : Type u_2} [partial_order α] [partial_order β] [order_bot α] [order_bot β] {x y : α × β} :

disjoint x y ↔ disjoint x.fst y.fst ∧ disjoint x.snd y.snd

source

@[protected]

theorem prod.codisjoint_iff {α : Type u_1} {β : Type u_2} [partial_order α] [partial_order β] [order_top α] [order_top β] {x y : α × β} :

codisjoint x y ↔ codisjoint x.fst y.fst ∧ codisjoint x.snd y.snd

source

@[protected]

theorem prod.is_compl_iff {α : Type u_1} {β : Type u_2} [partial_order α] [partial_order β] [bounded_order α] [bounded_order β] {x y : α × β} :

is_compl x y ↔ is_compl x.fst y.fst ∧ is_compl x.snd y.snd

source

@[simp]

theorem is_compl_to_dual_iff {α : Type u_1} [lattice α] [bounded_order α] {a b : α} :

is_compl (⇑order_dual.to_dual a) (⇑order_dual.to_dual b) ↔ is_compl a b

source

@[simp]

theorem is_compl_of_dual_iff {α : Type u_1} [lattice α] [bounded_order α] {a b : αᵒᵈ} :

is_compl (⇑order_dual.of_dual a) (⇑order_dual.of_dual b) ↔ is_compl a b

source

theorem is_compl_bot_top {α : Type u_1} [lattice α] [bounded_order α] :

is_compl ⊥ ⊤

source

theorem is_compl_top_bot {α : Type u_1} [lattice α] [bounded_order α] :

is_compl ⊤ ⊥

source

theorem eq_top_of_is_compl_bot {α : Type u_1} [lattice α] [bounded_order α] {x : α} (h : is_compl x ⊥) :

x = ⊤

source

theorem eq_top_of_bot_is_compl {α : Type u_1} [lattice α] [bounded_order α] {x : α} (h : is_compl ⊥ x) :

x = ⊤

source

theorem eq_bot_of_is_compl_top {α : Type u_1} [lattice α] [bounded_order α] {x : α} (h : is_compl x ⊤) :

x = ⊥

source

theorem eq_bot_of_top_is_compl {α : Type u_1} [lattice α] [bounded_order α] {x : α} (h : is_compl ⊤ x) :

x = ⊥

source

def is_complemented {α : Type u_1} [lattice α] [bounded_order α] (a : α) :

Prop

An element is complemented if it has a complement.

Equations

is_complemented a = ∃ (b : α), is_compl a b

source

theorem is_complemented_bot {α : Type u_1} [lattice α] [bounded_order α] :

is_complemented ⊥

source

theorem is_complemented_top {α : Type u_1} [lattice α] [bounded_order α] :

is_complemented ⊤

source

theorem is_complemented.sup {α : Type u_1} [distrib_lattice α] [bounded_order α] {a b : α} :

is_complemented a → is_complemented b → is_complemented (a ⊔ b)

source

theorem is_complemented.inf {α : Type u_1} [distrib_lattice α] [bounded_order α] {a b : α} :

is_complemented a → is_complemented b → is_complemented (a ⊓ b)

source

@[class]

structure complemented_lattice (α : Type u_2) [lattice α] [bounded_order α] :

Prop

exists_is_compl : ∀ (a : α), is_complemented a

A complemented bounded lattice is one where every element has a (not necessarily unique) complement.

Instances of this typeclass

source

@[protected, instance]

def complemented_lattice.order_dual.complemented_lattice {α : Type u_1} [lattice α] [bounded_order α] [complemented_lattice α] :

complemented_lattice αᵒᵈ

source

@[protected, instance]

def complementeds.partial_order (α : Type u_1) [lattice α] [bounded_order α] :

partial_order (complementeds α)

source

@[reducible]

def complementeds (α : Type u_1) [lattice α] [bounded_order α] :

Type u_1

The sublattice of complemented elements.

Equations

complementeds α = {a // is_complemented a}

source

@[protected, instance]

def complementeds.has_coe_t {α : Type u_1} [lattice α] [bounded_order α] :

has_coe_t (complementeds α) α

Equations

complementeds.has_coe_t = {coe := subtype.val (λ (a : α), is_complemented a)}

source

theorem complementeds.coe_injective {α : Type u_1} [lattice α] [bounded_order α] :

function.injective coe

source

@[simp, norm_cast]

theorem complementeds.coe_inj {α : Type u_1} [lattice α] [bounded_order α] {a b : complementeds α} :

↑a = ↑b ↔ a = b

source

@[simp, norm_cast]

theorem complementeds.coe_le_coe {α : Type u_1} [lattice α] [bounded_order α] {a b : complementeds α} :

↑a ≤ ↑b ↔ a ≤ b

source

@[simp, norm_cast]

theorem complementeds.coe_lt_coe {α : Type u_1} [lattice α] [bounded_order α] {a b : complementeds α} :

↑a < ↑b ↔ a < b

source

@[protected, instance]

def complementeds.bounded_order {α : Type u_1} [lattice α] [bounded_order α] :

bounded_order (complementeds α)

Equations

complementeds.bounded_order = subtype.bounded_order is_complemented_bot is_complemented_top

source

@[simp, norm_cast]

theorem complementeds.coe_bot {α : Type u_1} [lattice α] [bounded_order α] :

↑⊥ = ⊥

source

@[simp, norm_cast]

theorem complementeds.coe_top {α : Type u_1} [lattice α] [bounded_order α] :

↑⊤ = ⊤

source

@[simp]

theorem complementeds.mk_bot {α : Type u_1} [lattice α] [bounded_order α] :

⟨⊥, _⟩ = ⊥

source

@[simp]

theorem complementeds.mk_top {α : Type u_1} [lattice α] [bounded_order α] :

⟨⊤, _⟩ = ⊤

source

@[protected, instance]

def complementeds.inhabited {α : Type u_1} [lattice α] [bounded_order α] :

inhabited (complementeds α)

Equations

complementeds.inhabited = {default := ⊥}

source

@[protected, instance]

def complementeds.has_sup {α : Type u_1} [distrib_lattice α] [bounded_order α] :

has_sup (complementeds α)

Equations

complementeds.has_sup = {sup := λ (a b : complementeds α), ⟨↑a ⊔ ↑b, _⟩}

source

@[protected, instance]

def complementeds.has_inf {α : Type u_1} [distrib_lattice α] [bounded_order α] :

has_inf (complementeds α)

Equations

complementeds.has_inf = {inf := λ (a b : complementeds α), ⟨↑a ⊓ ↑b, _⟩}

source

@[simp, norm_cast]

theorem complementeds.coe_sup {α : Type u_1} [distrib_lattice α] [bounded_order α] (a b : complementeds α) :

↑(a ⊔ b) = ↑a ⊔ ↑b

source

@[simp, norm_cast]

theorem complementeds.coe_inf {α : Type u_1} [distrib_lattice α] [bounded_order α] (a b : complementeds α) :

↑(a ⊓ b) = ↑a ⊓ ↑b

source

@[simp]

theorem complementeds.mk_sup_mk {α : Type u_1} [distrib_lattice α] [bounded_order α] {a b : α} (ha : is_complemented a) (hb : is_complemented b) :

⟨a, ha⟩ ⊔ ⟨b, hb⟩ = ⟨a ⊔ b, _⟩

source

@[simp]

theorem complementeds.mk_inf_mk {α : Type u_1} [distrib_lattice α] [bounded_order α] {a b : α} (ha : is_complemented a) (hb : is_complemented b) :

⟨a, ha⟩ ⊓ ⟨b, hb⟩ = ⟨a ⊓ b, _⟩

source

@[protected, instance]

def complementeds.distrib_lattice {α : Type u_1} [distrib_lattice α] [bounded_order α] :

distrib_lattice (complementeds α)

Equations

complementeds.distrib_lattice = function.injective.distrib_lattice coe complementeds.distrib_lattice._proof_1 complementeds.coe_sup complementeds.coe_inf

source

@[simp, norm_cast]

theorem complementeds.disjoint_coe {α : Type u_1} [distrib_lattice α] [bounded_order α] {a b : complementeds α} :

disjoint ↑a ↑b ↔ disjoint a b

source

@[simp, norm_cast]

theorem complementeds.codisjoint_coe {α : Type u_1} [distrib_lattice α] [bounded_order α] {a b : complementeds α} :

codisjoint ↑a ↑b ↔ codisjoint a b

source

@[simp, norm_cast]

theorem complementeds.is_compl_coe {α : Type u_1} [distrib_lattice α] [bounded_order α] {a b : complementeds α} :

is_compl ↑a ↑b ↔ is_compl a b

source

@[protected, instance]

def complementeds.complemented_lattice {α : Type u_1} [distrib_lattice α] [bounded_order α] :

complemented_lattice (complementeds α)

mathlib3 documentation

Disjointness and complements #

Main declarations #