Theorems · Theorem · order theory

Concept.disjoint_extent_intent

∀ {α : Type u_2} {r' : α → α → Prop} {c' : Concept α α r'} [Std.Irrefl r'], Disjoint c'.extent c'.intent

Note that if r' is the ≤ relation, this theorem will often not be true!

Defined in

Mathlib.Order.Concept

Cited by

1 results in Mathlib

Foundations

Depth 60 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Std.Irrefl