structure
definition
def or abbrev
FiniteLogicalComparison
show as:
view Lean formalization →
formal statement (Lean)
25structure FiniteLogicalComparison (C : ComparisonOperator) : Prop where
26 identity : Identity C
27 non_contradiction : NonContradiction C
28 totality : ExcludedMiddle C
29 scale_invariant : ScaleInvariant C
30 nontrivial : NonTrivial C
31 counted_once_algebra : CountedOnceComposition C
32
33/-- Finite logical comparison supports truth-evaluable comparison. -/
used by (10)
-
finite_logical_comparison_forces_rcl -
finite_logical_has_counted_once -
finite_logical_has_finite_closure -
finite_logical_satisfies_laws -
finite_logical_to_operative -
finite_logical_to_truth_evaluable -
rcl_is_counted_once_logic_on_positive_ratios -
rcl_is_scale_free_counted_once_logic_on_positive_ratios -
scale_free_counted_once_logic_forces_ratio_rcl -
OperativeDomainStructure